perm filename TALK.3[TLK,DBL] blob
sn#158482 filedate 1975-05-06 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00027 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00004 00002 .DEVICE XGP
C00006 00003 .MACRO B ⊂ BEGIN VERBATIM GROUP ⊃
C00010 00004 .NSEC(Objective)
C00015 00005 .NSECP(Why Choose Math Research?)
C00018 00006 .NSECP(Potential Applications)
C00020 00007 .NSECP(Measuring Success)
C00021 00008 .NSECP(Experimenting with AM)
C00023 00009 .NSECP(Model of Math Research)
C00032 00010 .SSEC(Textbook-Order vs Research-Order)
C00050 00011 .SSEC(Metaphors to other processes)
C00057 00012 .NSECP(Knowledge AM Starts With)
C00062 00013 .NSECP(AM's Representation of Knowledge)
C00070 00014 .NSECP(Flow of Control in AM)
C00077 00015 .NSECP(Details: Getting AM going)
C00083 00016 .NSECP(Examples of Individual Modules)
C00097 00017 .NSECP(Example: The Modules Interacting)
C00101 00018 .SSEC(A Hypothetical Session)
C00108 00019 .SSEC(Comments on the Session)
C00111 00020 .SSEC(The Session Revisited: An In-Depth Example)
C00114 00021 .SSSEC(Looking at the new concept named "FACTORS")
C00128 00022 .SSSEC(Conjecturing the Unique Factorization Theorem)
C00139 00023 .SSSEC(Proving Existence)
C00150 00024 .NSECP(Timetable and Size of AM)
C00154 00025 .ASEC(Bibliography)
C00174 00026 .ASSEC(Articles)
C00183 00027 .COMMENT table of contents
C00184 ENDMK
C⊗;
.DEVICE XGP
.FONT 1 "BASL30"
.FONT 2 "BASB30"
.FONT 4 "BASI30"
.FONT 5 "BDR40"
.FONT 6 "NGR25"
.FONT 7 "NGR20"
.FONT 8 "GRFX35"
.FONT A "SUP"
.FONT B "SUB"
.TURN ON "↑α↓_π[]{"
.TURN ON "⊗" FOR "%"
.TURN ON "@" FOR "%"
.PAGE FRAME 54 HIGH 89 WIDE
.TITLE AREA HEADING LINES 1 TO 2
.AREA TEXT LINES 3 TO 53
.COUNT PAGE PRINTING "1"
.TABBREAK
.ODDLEFTBORDER←EVENLEFTBORDER←850
.AT "ffi" ⊂ IF THISFONT ≤ 4 THEN "≠" ELSE "fαfαi" ⊃;
.AT "ffl" ⊂ IF THISFONT ≤ 4 THEN "α∞" ELSE "fαfαl" ⊃;
.AT "ff" ⊂ IF THISFONT ≤ 4 THEN "≥" ELSE "fαf" ⊃;
.AT "fi" ⊂ IF THISFONT ≤ 4 THEN "α≡" ELSE "fαi" ⊃;
.AT "fl" ⊂ IF THISFONT ≤ 4 THEN "∨" ELSE "fαl" ⊃;
.SELECT 1
.MACRO B ⊂ BEGIN VERBATIM GROUP ⊃
.MACRO E ⊂ APART END ⊃
.MACRO D ⊂ ONCE PREFACE 100 MILLS ⊃
.MACRO BB ⊂ BEGIN FILL ADJUST SINGLE SPACE PREFACE 1 INDENT 0,4,0 ⊃
.MACRO BGIV ⊂ BEGIN NOFILL SELECT 7 INDENT 0 PREFACE 0 TURN OFF "{}" TURN ON "↑↓" ⊃
.MACRO B0 ⊂ BEGIN WIDEN 0,7 SELECT 8 NOFILL PREFACE 0 MILLS TURN OFF "↑↓α" GROUP ⊃
.MACRO FAD ⊂ FILL ADJUST DOUBLE SPACE PREFACE 2 ⊃
.MACRO FAS ⊂ FILL ADJUST SINGLE SPACE PREFACE 1 ⊃
.FAD
.MYFOOT←1
.FOOTSEP←"________________________________________________________________________________________"
.COUNT FOOTNOTE INLINE PRINTING "⊗A1⊗*"
.AT "$$" ENTRY "*" ⊂ XGENLINES←XGENLINES-1; NEXT FOOTNOTE; !;
.SEND FOOT ⊂ TURN ON "[]{" SELECT 7; SPACING 0; PREFACE 0; INDENT 0,10
⊗A{MYFOOT}⊗* ENTRY
.MYFOOT←MYFOOT+1
.BREAK ⊃ ⊃
.MACRO NSECP(A) ⊂ SSECNUM←0
.SECNUM←SECNUM+1
.SECTION←"A"
.SKIP TO COLUMN 1
.TURN ON "{∞→"
.SEND CONTENTS ⊂
@1{SECNUM}. A⊗* ∞.→ {PAGE}
.⊃
.TURN OFF "{∞→"
.ONCE CENTER TURN ON "{}"
@5↓_{SECNUM}. A_↓⊗*
. ⊃
.MACRO ASEC(A) ⊂ SSECNUM←0
.SECTION←"A"
.SKIP TO COLUMN 1
.TURN ON "{∞→"
.SEND CONTENTS ⊂
@1 A⊗*
.⊃
.TURN OFF "{∞→"
.ONCE CENTER TURN ON "{}"
@5↓_A_↓⊗*
. ⊃
.MACRO NSEC(A) ⊂
.SSECNUM←0
.SECNUM←SECNUM+1
.TURN ON "{∞→"
.SEND CONTENTS ⊂
@1{SECNUM}. A⊗* ∞.→ {PAGE}
.⊃
.TURN OFF "{∞→"
.SECTION←"A"
.GROUP SKIP 3
.ONCE CENTER TURN ON "{}"
@5↓_{SECNUM}. A_↓⊗*
. ⊃
.MACRO SSEC(A) ⊂ TURN ON "{∞→"
.SSECNUM←SSECNUM+1
.SSSECNUM←0
.SEND CONTENTS ⊂
@7 A⊗* ∞.→ {PAGE}
.⊃
.TURN OFF "{∞→"
.ONCE INDENT 6 TURN ON "{}"
@2↓_{SECNUM}.{SSECNUM}. A_↓⊗*
. ⊃
.MACRO ASSEC(A) ⊂ TURN ON "{∞→"
.SEND CONTENTS ⊂
@7 A⊗*
.⊃
.TURN OFF "{∞→"
.ONCE INDENT 6 TURN ON "{}"
@2↓_A_↓⊗*
. ⊃
.MACRO SSSEC(A) ⊂ TURN ON "{∞→"
.SSSECNUM←SSSECNUM+1
.TURN OFF "{∞→"
.ONCE INDENT 1 TURN ON "{}"
@2↓_{SECNUM}.{SSECNUM}.{SSSECNUM}. A_↓⊗*
. ⊃
.SECNUM←0
.SELECT 1
.INSERT CONTENTS
.PAGE←0
.PORTION THESIS
.TURN OFF "{∞→}"
.PAGE←0
.NEXT PAGE
.INDENT 0
.FAD
.TURN OFF "{∞→}"
.ONCE CENTER
.NSEC(Objective)
.EVERY HEADING(⊗7Automated Math Theory Formation,Doug Lenat,{DATE} page {PAGE}⊗*)
I've spent the last six months
considering theory formation in mathematics:
how math researchers propose interesting
hypotheses, test them, and develop them into interesting theories.
The experimental ⊗4vehicle⊗* of my research is
a system, a program called AM
(for ⊗2↓_A_↓⊗*utomated ⊗2↓_M_↓⊗*athematician),
which can actually do mathematical research:
propose axiomatizations,$$ Based on AM's earlier successes and/or on simulated
real-world situations *
propose and prove conjectures,$$ Using the
heuristics discussed by Polya *
use intuition$$ Intuition
will mean visual analogies to simulated real-world scenarios *
to justify beliefs and to
understand new observations, evaluate concepts and theories for aesthetic interest,
and use such judgments to guide development in the most promising direction.
AM is completely specified on paper; this coming month I'll be programming it;
starting in a few months it will be sufficiently debugged to start experimenting
with it.
More specifically, AM will be given 150 particular ⊗4premathematical⊗*
concepts,$$
Universal, fundamental, prenumerical knowledge. This includes:
elementary notions of sets, relations, properties, problems, problem-solving,
methods, proof techniques, analogy; and also some abilities
to evaluate interestingness, to locate relevant knowledge *
and will hopefully
develop the notion of Cardinality, which paves the way to the domain
of (elementary) number theory.
Eventually, AM may develop enough mathematical systems to
notice a common structure, which will be abstracted into something like the
group axioms. This might then lead into developing elementary abstract algebra.
Such a proposal immediately raises many questions; they are listed below, and
each one is then dealt with in a separate section.
.BEGIN NOFILL INDENT 3 PREFACE 1 SELECT 2 GROUP
Why choose mathematics research as the domain for investigating theory formation?
What are some potential concrete applications of this project?
How will the success of the system be measured?
What experiments can be done on AM?
What is our model of math research? ⊗7To automate something, you must have a good model for it.⊗*
What given knowledge will AM initially start with?
How will this knowledge be represented?
What is the control mechanism; what does AM "do"?
Examples of individual knowledge modules.
Examples of communities of modules interacting, developing new modules.
What is the timetable for this project? What is the current state?
.END
.EVERY HEADING(⊗7Automated Math Theory Formation,Doug Lenat,{DATE} page {PAGE}⊗*)
.NSECP(Why Choose Math Research?)
As the DENDRAL project illustrated so clearly, choice of subject domain is
quite important when studying how researchers discover and develop their theories.
Mathematics has been chosen as the domain of this investigation, because
(i) In doing math research, one needn't cope with
the uncertainties and fallability of testing equipment;
that is, there are nouncertainties in the data this way;
(ii) Reliance on experts' introspections is one of the most powerful techniques
for codifying the judgmental criteria necessary to do effective work in a field;
I am somewhat of an expert in mathematics, hence won't have to rely on external
sources for guidance.
(iii) A hard science is of course easier to work in than a soft one; to
automate research into psychology would require more knowledge about
human information processing than now is known, because psychology deals with
entities as complex as you and I. Also, in a hard science, the ⊗4languages⊗* to
communicate information can be simple even though the
⊗4message⊗* itself is sophisticated.
(iv) A reason which exists to a lesser degreee than would be expected:
Since mathematics can deal with any conceivable constructs, a researcher there is
not
limited to explaining observed data.
It turns out, however, that most unmotivated forays are fruitless:
reality ⊗4is⊗* the most common
inspiration of successful, interesting mathematical theories.
.NSECP(Potential Applications)
(i) The modular representation of knowledge that AM uses might prove to be effective
in other large knowledge-based systems.
(ii) Most of the particular heuristic judgmental criteria for interestingness,
utility, etc., might be valid in developing theories in other sciences.
(iii) If the repertoire of intuition (simulated real-world scenarios)
is sufficient for AM to develop elementary concepts of math, then educators
should ensure that children (4-6 years old) are thoroughly exposed to those
scenarios.$$ These tentatively include situations like seesaws, slides,
piling marbles into pans of a balance scale, comparing the heights of towers
built out of cubical blocks, solving a jigsaw puzzle, etc.*
(iv) We might learn something about how the theory formation task changes
as the theory grows in sophistication. For example, can the same methods which
lead AM from premathematical concepts to arithmetic also lead AM from
there to abstract algebra? Or are a new set of intuitions or criteria required?
.NSECP(Measuring Success)
(i) By its achievements: Compare the list of concepts and methods it develops
against the list of concepts and methods it began with.
(ii) By the route AM took to accomplish these advances: How clever, how circuitous,
how many of the detours were quickly identified as such and abandoned?
(iii) By the character of the User--System interactions: How important is the user's
guidance? How closely must he guide AM? What happens if he doesn't say anything ever?
When he does want to say something, is there an easy way to express that to AM,
and does AM respond well to it?
.NSECP(Experimenting with AM)
Assume that AM has been written, and has in fact developed some new$$
New to AM, not to the world. It would be quite accidental if AM proved
theorems unknown to Mankind.*
concepts on its own.
Here is a list of some of the more interesting experiments that would be
possible to perform, using AM:
(i) Remove individual concept modules. Is performance noticably degraded?
Which concepts does AM now "miss" discovering? Is the removed concept
later discovered anyway by those which are left in AM? This should indicate
the importance of each kind of concept (and method) which AM starts with.
(ii) Vary the relative weights given to features by the criteria which judge
aesthetics, inteestingness, worth, utility, etc. See how important each factor
is in directing AM along successful routes.
(iii) Add several new concept modules (and a few new intuitions) and see if AM
can work in some unplanned field of mathematics (like geometry or analysis).
(iv) Add several new intuitions, and see if AM can develop nonmathematical
theories (elementary physics, elementary physics). This would also require
modifying AM's freedom to "ignore a given bodyof data and move on to something
more interesting".
.NSECP(Model of Math Research)
In order to intelligently discuss how to automate an activity, we must be very
clear about how humans do that activity. Thus, for AM, we must begin by hypothesizing
a particular model of how mathematicians actually go about doing their research.
After presenting our model, we can then discuss how to automate the processes
involved.
Thanks to Polya, Kersher, Hadamard, Skemp, and many others,
such a model for math theory formation can be pieced together:
.BEGIN INDENT 0,3,0
.ONCE SELECT 8 TURN OFF "α" TURN ON "∞→"
⊂∞α→⊃
.NARROW 2,2 SINGLE SPACE PREFACE 0
1. The order of events in a typical mathematical investigation is:
Observe →→→ Notice Regularity →→→ Formalize →→→ Develop the theory.
The observation is either of reality or an analogous, already-established
mathematical theory. Thus math research is an ⊗4empirical⊗* process.
2. The key to keeping this from becoming a blind, explosive search is the
proper use of evaluation criteria. That is, one must constantly choose the
most interesting, aesthetically pleasing, useful,... concept to expand next.
This is analogous to Dendral's reliance on good heuristics to constrain the
structure generator.
3. The non-formal criteria (aesthetics, interestingness, intuitive clarity,
utility, analogy, empirical evidence) are much more important than formal
deductive methods in developing mathematically worthwhile theories.
4. The above criteria are virtually the same in all domains of mathematics,
and at all levels. Each factor sometimes encourages investigation in a certain
area, and sometimes discourages further effort.
5. For true understanding, AM must understand$$ Have access to, relate to, store,
be able to manipulate, be able to answer questions about *
each concept in several ways:
declarative (definition), operational (how to use it), demonic (recognizing
when it is relevant), exemplary (especially boundary examples), and
intuitive (opaque image of a real-world interpretation).
6. Progress in ⊗4any⊗* field of math demands much intuition (and some
formal knowledge) of ⊗4many⊗* different mathematical fields. So a broad,
universal core of intuition must be established before any single theory
can meaningfully be developed.
.WIDEN 2,2
.ONCE SELECT 8 TURN OFF "α" TURN ON "∞→"
%∞α→$
.END
.SSEC(Details)
This last point (6) merits elaboration. I believe that to develop any given field
of mathematics, one must possess much intuition about each
⊗4psychologically⊗* prerequisite field,$$ One which makes the new field
easier to learn, which contains more concrete analogues of the ideas of the new
field. For example, knowing about geometry makes it easier to learn about
topology, even though topology never formally uses any results or definitions
from geometry. * and some definite facts about each ⊗4formally⊗* preceding
field$$ For example, arithmetic is usually formally based upon set theory,
although most of us learn about them in the other order * of mathematics.
The diagram here
indicates the prerequisites for each domain which might
conceivably be worked in by AM. To start in a given domain, some knowledge
should exist about all domains which point to the given one,
about all domains which point to ⊗4them⊗*, etc.
.B0
Elementary Logic ααα→ Theorem-Proving ααααααααααααααα⊃
↑ ~
~ ~
~ ~
εαααααααα→ Geometry ααα→ Topology ~
~ ~ ↑ ~ ~
~ ~ ~ ~ ~
~ ↓ ~ ↓ ~
~ Analytic Geometry ~ Algebraic Topology ~
~ ↑ ↓ ↑ ~
~ ~ Measure Theory ~ ~
↓ ~ ↑ ~ ~
Boolean Algebra αβαβαα→ Abstract Algebra ~
↑ ~ ~ ~ ↓
.ONCE TURN ON "α"
~ ~ ↓ ~ Program Verification
~ Analysis ↓ ↑
~ ↑ Concrete Algebra ~
~ ~ ↑ ~
~ ~ ~ ~
↓ ~ ~ ~
Set Theory ααα→ Arithmetic ααα→ Number Theory ~
~ ~
~ ~
↓ ~
Combinatorics ←ααα→ Graph Theory αααα$
.E
Each arrow represents either a psychological or a formal prerequisite:
to work in the field pointed to, one should know something about the field
pointed from.
Notice that almost all the "elementary"
branches of mathematics are either formally
or psychologically prerequisite
to each other.$$ For example, one should have some intuition about
sets before doing Number theory,
and one should have some intuition about numbers
and counting before doing Set theory. * So a broad foundation of intuition,
spanning ⊗4↓_several_↓⊗* mathematical and
real-world concepts, is prerequisite to sophisticated behavior in ⊗4any⊗*
branch of mathematics.
This seems like the idea of a "critical mass" of knowledge,
so often sensationalized in science fiction. In addition to
expecting that the corpus must exceed some minimum absolute size,
I am claiming that it must also exceed some minimum degree of richness, of breadth.
.SSEC(Textbook-Order vs Research-Order)
Let us elaborate on point (1) above. The idea there is that
the order in which a math textbook presents a theory is almost the exact
opposite of the order in which it was actually discovered and developed.
.B0 INDENT 10
PRIMITIVES, AXIOMS ααααα→ DEFINITIONS ←αααααααααααααα⊃
~ ~
~ ~
↓ ~
STATEMENT OF LEMMA ~
~ ~
~ ~
↓ ~
PROOF OF LEMMA ~
~ ~
~ ~
↓ ~
~ ~
~ ~
↓ ~
STATEMENT OF NEXT LEMMA ~
~ ~
| ~
| ~
| ~
| ~
| ~
↓ ~
PROOF OF LAST LEMMA ~
~ ~
~ ~
↓ ~
STATEMENT OF THEOREM ~
~ ~
~ ~
↓ ~
PROOF OF THEOREM ααααααααααααααα$
.E
In a textbook, one introduces some primitive elements of the theory, postulates
some axioms relating these objects and operations, then enters a
⊗4"Define → State → Prove⊗*" loop. Lemmas are stated and proved before the
theorems which require them. Motivations of any kind are a rareity, and often
are mentioned parenthetically as an application of a theorem which has just been
proved.
As an example, here is how my sophomore textbook was organized:
.B0
.INDENT 10
Set N, Op S:N→N,
Peano⊗1'⊗*s Axioms αααααα→ Define +
~
.TURN ON "α"
↓
State some property of +
~
↓
Prove this propterty
|
|
|
Define ⊗6≤⊗*
|
|
|
Define g.l.b
~
~
↓
State that glb always exists
~
↓
Prove this claim
|
|
|
Define TIMES
Define ⊗5Z⊗*
|
|
|
Define DIVIDES
Define PRIME
~
↓
State Euclid⊗1'⊗*s Algorithm
~
↓
Prove Euclid⊗1'⊗*s Algorithm
.E
It began by presenting Peano's axioms, completely unmotivated, then entered
the the Define → State → Prove loop. For example, the two concepts of
⊗4prime⊗* and ⊗4non-factorizable number⊗* are defined separately,
even though a hundred pages elapse before any mathematical system is presented
in which the two notions don't completely coincide.
This psychic ordering is repeated,
in microcosm, in each textbook proof. For example,
a typical epsilon/delta argument will start by magically proposing some function
delta(epsilon), which is just the right one for the approximations taken later.
In contrast,
a mathematician doing research works in almost the opposite order.
.B0 INDENT 0
OBSERVE x ααααα→ NOTICE SOME INTERESTING REGULARITIES
~
~
↓
GATHER UP ALL RELATED INTERESTING RELATIONSHIPS
~
~
↓
STATE THESE FORMALLY
~
~
↓
CHOOSE THE MOST INTUITIVELY OBVIOUS OF THESE
~
~
↓
TRY TO DERIVE ALL THE REST FROM THIS CORE
~
~
↓
IF THE CORE IS INCONSISTENT, ELIMINATE THE LEAST BELIEVED MEMBERS
IF ANY CAN'T BE DERIVED: ENLARGE THE CORE SO THAT THEY CAN BE
IF ANY MEMBER OF THE CORE CAN BE DERIVED FROM THE OTHERS, ELIMINATE IT
~
~
↓
CALL THE CORE "AXIOMS", AND THE REST "THEOREMS"
~
~
↓
TRY TO DERIVE PREVIOUSLY UNSUSPECTED THEOREMS, FORMALLY
IF SO: TRY TO REINTERPRET IN TERMS OF x
TRY TO FIND NEW RELATIONSHIPS OCCURRING IN x
IF SO: TRY TO PROVE THEM USING THE EXISTING AXIOMS AND THEOREMS
.E
The researcher begins by observing the world: he looks at scenarios from reality
and perhaps also some earlier, already-developed,interesting mathematical theories.
He notices some interesting facts, either by raw perception of regularities
or by analogy to some interesting pattern in another theory. Of these observations,
he chooses a small set of the most intuitively clear ones, and tries to derive the
other observations formally from this chosen core. After several passes, he will
succeed; the final chosen core he calls axioms, and the rest he calls theorems.
$$ Once axiomatized, new theorems may be proposed syntactically: the researcher then
may check each conjecture against the roots of the theory (both real-world and
analogous). Additional observations can later be checked against the theory,
to see if they also can be derived from the axioms.*
Let's make this more concrete, by considering how a mathematician might discover
and develop the simplest numerical concepts, the ones my textbook introduced
and developed in such a polished way.
Let's say that he possesses our previously-mentioned prenumerical background.
He begins by considering the two activities:
Comparing piles of marbles using a pan balance, and comparing the heights of
towers constructed from toy blocks.
.B0 INDENT 7
/~\ /~\
/ ~ \ / ~ \
/ ~ \ / ~ \
/ ~ \ / ~ \
/ ~ \ / ~ \
/ ~ \ / ~ \
/ ~ \ oo / ~ \ oo
αααα/ ~ \αααα αααα/ ~ \αααα
~ ~
~ ~
~ ~
αααααααααααα∀αααααααααααα αααααααααααα∀αααααααααααα
/~\
/ ~ \
/ ~ \
/ ~ \ o
/ ~ \αααα
/ ~
/ ~
/ ~
/ ~
ooo / ~
αααα/ ~
~
ααααααααααααααααααααααααα
************************************************************************************
αααααα⊃
|
⊂ααααα⊃ |
~ ~ |
~ ~ |
εαααααλ |
~ ~ | αααααα⊃
~ ~ | |
εαααααλ | ⊂ααααα⊃ |
~ ~ | ~ ~ |
~ ~ ~ ~
%ααααα$ %ααααα$
.E
When he tires of playing, the mathematician makes a list of the most basic
features of these situations.
.BEGIN NOFILL SELECT 1 PREFACE 0 INDENT 0 TABS 44,85 TURN ON "\" GROUP
.ONCE CENTER
FUNDAMENTAL CONCEPTS
.TURN ON "→"
ABOUT WEIGHING MARBLES:\ABOUT PILING BLOCKS: →COMMON NAME:
There are some marbles to play with.\There are some blocks to play with.→ele
The marbles are indistinguishable.\The blocks are indistinguishable.→set
Besides individual marbles, we can\Besides individual blocks, we can→var n
talk about a pile of marbles as a unit.\talk about a tower of blocks as unit.
We can copy a given pile.\We can copy a given tower.→copy C
A pile of marbes and a copy of\A tower of blocks and a copy of
that pile are indistinguishable.\that tower are indistinguishable.→ignore C
To make pile heavier, add a marble.\We can stack another block onto a tower.→succ S
Lighten pile by removing a marble.\Can shorten tower by removing top block.→pred P
We can tell if piles x,y balance.\Can see if towers x,y are same size.→equal =
Can tell if pile x is heavier than y.\We can see if tower x is higher than y.→⊗6>⊗*
We can add one pile to another.\We can stack one tower on top of another.→add +
Can remove a pile from a big one.\Can lift a tower off top of a big one.→sub -
Can remove any marble from pile.\We can only remove topmost blocks.→pop
Pile might have no marbles.\There might be no blocks in a tower.→zero 0
Can replace each marble in a pile\We can replace each block in a tower
by a copy of some other pile.\by a copy of some other tower.→mult x
A lone marble is also a pile.\A lone block is also a tower.→one 1
etc.\etc.→etc.
***********************************************************************************
.E
These correspond to the objects and operators of the theory he is about to develop.
He gives them each a name; I have permitted him to choose the common name for
each concept, but that doesn't matter, of course. Notice that most of these
are not usually considered primitive at all.
The next list he draws up contains several specific observations, translated from
the blocks/marbles manipulation language into these new symbols.
The relationship is translated from these symbols into the
⊗4other⊗* scenario's language, and checked. Thus all the observations here are
meaningful in both of the manipulative domains:
.BEGIN NOFILL SELECT 6 PREFACE 0 INDENT 0 TABS 15,30,45,60,75 TURN ON "\" GROUP
******************************************************************************************
0=0\1=1\¬(0=1)\¬(1=0)\¬(S(1)=1)\¬(0=S(0))
S(0)=1\1=S(0)\S(0)=S(0)\S(1)=S(1)\¬(S(0)=S(1))\¬(S(1)=S(0))
0+0=0\1+1=S(1)\0+1=1\1+0=1\S(1)+0=S(1)\S(0)+S(0)=S(1)
0x0=0\1x1=1\0x1=0\1x0=0\S(S(1))x0=0\S(S(1)x1=S(S(1))
1>0\S(1)>1\S(1)>0\¬(0>1)\¬(1>1)\¬(0>0)
******************************************************************************************
.E
Now comes some simple generalization, either directly from the scenarios,
perceptaully from the list just compiled, or syntactically from that list
(e.g., by replacing constants by variables).
Again, each of these generalizations
is intuitively checked in both real-world domains.
.BEGIN NOFILL SELECT 6 PREFACE 0 INDENT 0 TABS 15,30,45,60,75 TURN ON "\" GROUP
******************************************************************************************
If n>0, then D(n) can be performed; else D(n) cannot be performed.
If n>0, then n>D(n)\S(n)>n\\S(n)=n+1\S(S(n))>n
If n=m then S(n)=S(m)\\\If S(n)=S(m) then n=m
D(S(n))=n\\If n>0 then S(D(n))=n\If n>0 then n+m>m
m+S(n)>m\\If n=m then ¬(n>m)\If n>m then ¬(n=m)
If n=m ∧ n>r then m>r\n=n\¬(n>n)\¬(n=S(n))
If n>m ∧ m>r then n>r\If n=m ∧ m=r then n=r\If n=m ∧ r=m then r=n
If n=m then m=n\If n>m then ¬(m>n)\n>m ∨ m>n ∨ n=m
nxm = mxn\\nxS(m)=nxm + n\\n+m=m+n
n+S(m)=S(n)+m\\(n+m)+(r+s) = n+((s+m)+r)
nx(mxr)=(nxr)xm\S(n)+D(m)=m+n
etc.
**********************************************************************************
.E
Some of these are now considered as axiomatic, as defining the operations and
structures involved; the rest are considered secondary, as theorems following from
the axioms. This process is a slow search.
The most important game is not "finding minimal axiom sets", but rather
"what else can we prove from this set of axioms and theorems".
The AM research goal is to learn how to play this game of theory development.
To summarize idea (1):
The ⊗4motivation⊗* for a new mathematical development is either:
(a) looking at reality and at the mathematics
you have already$$ Then abstract out some interesting features;
formalize those into a
specific set of primitive structures and relations and axioms about those
basic entities *, or (b) given an existing theory, propose some new conjecture or
definition, based on analogy to the real-world roots of this theory,$$ Based
on patterns perceived in empirical
evidence * or based on analogy to a known interesting theorem in another theory,
or occasionally based only on applying some fruitful method and observing the
result.
.SSEC(Metaphors to other processes)
Let's consider some alternate ways of looking at such theory development, some
analogies to processes with which you're probably more familiar.
.SSSEC(Growing a tree, using heuristic constraints)
Once motivated, the idea is developed and evaluated. At each moment, the
researcher should be working on the most promising of all the proposed ideas.
This process is thus a sophisticated expansion of a tree,
where new conceptual nodes are
"grown" in the most promising area, and where barren dead-ends are eventually
"pruned". To do mathematical research well, it is thus necessary and sufficent
to have good methods for proposing new concepts from existing ones, and for
deciding how interesting each candidate is. That is: effective growing and pruning
strategies.
.SSSEC(Exploring a space using an evaluation function)
Consider our core of premathematical knowledge.
By compounding the known concepts and methods,$$Using
abstraction from reality, analogy with existing theories,
the postulational method, and problem-solving techniques *
we can extend this
foundation a little wherever we wish.
⊗4<Visualize: SEVERAL SHORT LINES IN BLACK, EMANATING
FROM A CENTRAL CORE>⊗*.
The incredible variety of alternatives to investigate includes
all known mathematics, much trivia, countless deadends, and so on.
The only "successful" paths near the core
are the narrow ribbons of known mathematics
(perhaps with a few undiscovered other slivers).
⊗4<Visualize SNAKE-LIKE LINES IN RED, twisting away from the core, intersecting>⊗*.
How should we walk through this immense space, with any hope of following the
few, slender branches of already-established mathematics (or some equally successful
new fields)? We must do hill-climbing; as new concepts are formed, decide how
promising they are, always explore the currently most-promising new concept. The
evaluation function is quite nontrivial, and this research may be viewed as an
attempt to study and explain and duplicate the judgmental criteria people employ.
The impportant visualization to make
is that with proper evaluation criteria, we convert the
flat picture to
a breath-taking relief map:
the known lines of development become
mountain ranges, soaring above the vast flat plains
of trivia and inconsistency
below.
Occasionally an isolated
hill is discovered near the core;$$ E.g.,
Knuth's ↓_Surreal Numbers_↓ * certainly
whole ranges lie undiscovered for long periods of time:$$ E.g.,
non-Euclidean geometries * the terrrain far from the initial core is
not at all explored.
Intuition is like vision, letting the explorer observe a distant mountain,
long before he has conquered its intricate, specific challenges.
If the criteria for evaluating interestingness and promise are good enough, then
it should be straightforward to simply push off in any direction, locate some
nearby peak, and follow the mountain range along (duplicating the development in
some field). In fact, by intentionally pushing off in apparently barren directions,
new ranges might be enountered. If the criteria are "correct", then ⊗4any⊗* new
discovery the system makes and likes will necessarily be interesting to humans.
If, as is more likely, the criteria are deficient, this too will tell us much. Before
beginning, we shall strive to include all the obvious factors which enter into
judgmental decisions, with appropriate weights, etc. If the criteria fail, then
we can analyze that failure and learn about one nonobvious factor in evaluating
success in mathematics (and in any creative endeavor). After modifying the criteria
to include this new factor, we can proceed again.
.SSSEC(Syntax and Semantics in Natural Language Processing)
One final analogy: Consider assumptions, axioms, definitions, and
theorems to be
syntactic rules for the
language that we call Mathematics.
Thus theorem-proving, and the whole of textbook mathematics, is a purely syntactic
process.
Then these judgmental
criteria I am alluding to would correspond to the semantic knowledge associated
with these more formal methods.
Just as one can upgrade natural-language-understanding by encorporating semantic
knowledge, so AM ensures that it knows the intuitive and empirical roots of
each concept in its repertoire.
.NSECP(Knowledge AM Starts With)
At each stage, AM has some set of concepts (represented as modules,
clumps of information). Its ativity is to fill out the existing clumps
more, and develop new clumps. Each clump is called a BEING. Here are
the names of the BEINGs (concepts, clumps, ... ) which AM will start with:
.BEGIN FILL SELECT 6 SINGLE SPACE PREFACE 0 TURN OFF "{}-"
.INDENT 3,7,0
.ONCE PREFACE 3 FLUSH LEFT
(i) ⊗2Objects⊗*
Ordered-pair,
Variable,
Propositional-constant,
Structure,
List-structure,
Bag-structure,
Set-structure,
Assertion,
Axiom
.ONCE PREFACE 2 FLUSH LEFT
(ii) ⊗2Actives⊗*
Operations: Compose, Insert, Delete, Convert-structure, Substitute, Assign,
Map-structure,
Undo,
Reverse-ordered-pair, Rule-of-inference, Disjoin, Conjoin, Negate,
Imply, Unite, Set-union, Cross-product, Common-parts, Set-intersection,
Set-difference, Put-in-order, Abstract-out-similarities, Contrast
Relations: Equality, Membership, Containment, Equivalence,
Equipollence,
Scope,
Quantification, ⊗7For-all, There-exists, Not-for-all, Never, Only-sometimes⊗*
Properties: Ordered, Extreme, Properties-of-Activities
.ONCE PREFACE 2 FLUSH LEFT
(iii) ⊗2Higher-order Actives⊗*
Find, Select, Guess, Ellipsis, Analogize, Conserve, Approximate
Examine, Test, Assume, Judge,
Define,
Prove, ⊗7Logically-deduce, Prove-directly, Cases,
Working-backwards, Prove-indirectly, Prove-universal-claims, Mathematical-induction,
Prove-existential-claims,
Prove-existence-constructively, Prove-existence-deductively,⊗*
Disprove, ⊗7Disprove-constructively, Disprove-indirectly,⊗*
Solve-problem, Debug, Trial-and-error, Hill-climb, Subgoal, Work-indirectly,
Relations-between-problems
Communicate, Communicate-with-user, Translate-into-English-for-User,
Translate-from-English-for-concepts, User-model, Communicate-among-concepts,
Infer-from-examples, Select-representation
Isomorphism, Categoricity, Canonical, Interpretation-of-theory
.ONCE PREFACE 2 FLUSH LEFT
(iv) ⊗2Higher-order Objects⊗*
Statement, Conjecture, ⊗7Statement-of-generality, Statement-of-existence,⊗*
Theorem, Proof, Counterexample, Contradiction, Analogy, Assumption
Problem, Problem-to-find, Problem-to-prove, Problem-to-creatively-define,
Action-problem, Inference-problem, Bug
Representation, Symbolic-representation, Diagram, Scenario
Mathematical-theory, Foundation, Basis, Formal-system
.END
.ONCE PREFACE 3
Of course, we must ask ⊗4precisely⊗* what AM knows about each of these concepts.
But to fully answer that, we must digress and discuss how the knowledge
is represented. We must explain the modular BEINGs scheme for representing
information about a concept.
.NSECP(AM's Representation of Knowledge)
AM will represent each
concept as a bundle of facets (DEFINITION, INTUITION, RECOGNITION,
INTERESTINGNESS,...), and each facet will be stored internally as a
little program. Each concept will have precisely the same set of
facets. This enables us to assemble, in advance, a body of knowledge
(called ⊗2strategic⊗* knowledge) about each facet. Each concept is called
a BEING$$
For historical reasons. BEINGs is a modular scheme for representing
knowledge, akin to ACTORs,
PANDEMONIUM, SMALLTALK,
CLASSes, and FRAMEs. Details
about the origin of the BEINGs ideas,
can be found in [Green et al] and in [Lenat].*.
Depending
on how you want to visualize a BEING, these subdivisions can be called
parts, questions, facets, or slots.
Part P of BEING B will be abbreviated as B.P.
.SSEC(Facets that each concept might have)
Each facet program can be viewed as answering a certain family of questions
about the BEING (concept) in which it is embedded$$ For example, the DEFINITION
facet of COMPOSE should be able to tell if any given entity is a composition.*.
Below is the tentative set of facets that concepts can have, followed by a
brief description of what question(s) each facet answers:
.SKIP TO COLUMN 1
.BEGIN FILL SELECT 7 PREFACE 0 SPACING 0 INDENT 15 GROUP
.ONCE FLUSH LEFT PREFACE 1
⊗4RECOGNITION GROUPING⊗* Notice when this BEING, call it B, is relevant.
CHANGES Is this rele. to producing the desired change in the world?
FINAL What situations is this BEING rele. to bringing about?
PAST Where is this used frequently, to advantage?
IDEN {not}{quick} {fast} tests to see if this BEING is {not} currently referred to
.ONCE FLUSH LEFT
⊗4ALTER-ONESELF GROUPING⊗* Know about variations of yourself, how good you are, etc.
GENERALIZATIONS What is this a special case of? How to make this more general.
SPECIALIZATIONS Special cases of this? What new properties exist only there?
BOUNDARY What marks the limits of this concept? Why exactly there?
DOMAIN/RANGE {not} Set of (what one can{'t} apply it to, what kind of thing one {never} gets)
ORDERING(Complete) What order should the parts be concentrated on (default)
WORTH Aesthetic, efficency, complexity, ubiquity, certainty, analogic utility, survival basis
INTEREST What special factors make this type of BEING interesting?
JUSTIFICATION Why believe this? Formal/intu. For thms and conjecs. What has been tried?
OPERATIONS Properties associated with BEING. What can one do to it, what happens then?
.ONCE FLUSH LEFT
⊗4ACT-ON-ANOTHER GROUPING⊗* Look at part of another BEING, and perhaps do something to it.
⊗1CHANGE⊗* subgrouping of parts:
BOUNDARY-OPERATIONS {not} Ops rele. to patching {messing}up not-bdy-entities {bdy-entities}
FILLIN How to initially fill it in, when and how to augment what is there already.
STRUCTURE Whether, When, How to retructure (or split) this part.
ALGORITHMS How to compute this, do this activity. Related to Representation.
⊗1INTERPRET⊗* subgrouping of parts:
CHECK How to examine and test out what is already there.
REPRESENTATION How should entities of type B be structured internally? Contents' format.
VIEWS (e.g., How to view any Active as an operator, function, relation, property, corres., set of tuples)
.ONCE FLUSH LEFT
⊗4INFO GROUPING⊗* General information about this BEING, B, and how it fits in.
DEFINITION Several alternative formal definitions of this concept. Can be axiomatic, recursive.
INTU Analogic interp., ties to simpler objects, to reality. Opaque.
TIES Alterns. Parents/offspring. Analogies. Associated thms, conjecs, axioms, specific BEING's.
EXAMPLES {not} {bdy} Includes trivial, typical, and advanced cases of each type.
CONTENTS What is the value stored here, the actual contents of this entity.
.END
.FAD
.XGENLINES←XGENLINES+2
Let us take the organization sketched above as ⊗4literal⊗*; thus all knowledge in the
system is organized in packets called "BEINGs",
with each BEING containing all the relevant facts and ideas about one single concept.
Each BEING has about 25 different slots or "parts",
with each part having a name and a value. One interpretation of this is that
the name represents a question, and the value represents how to answer that question.
The BEINGs are organized into five categories or "families",
each containing about 30 BEINGs
to start with. The slots are organized into four categories, each with about
6 differently-named slots.
There is one distinguished structure, called CS (for Current Situation), which
holds pointers to all the recent system activities, notably those which have been
suspended, relevant new information, goals outstanding, BEINGs which were recently
judged interesting but haven't been worked on since then, recent comments from the
user, etc.
.NSECP(Flow of Control in AM)
.SELECT 1
Control in the system: As AM runs, at each moment, each concept
will have only a few of its facet programs filled in; most of the
facets of most of the concepts will be unknown. AM's only control
structure is to repeatedly choose some facet of some concept
(some part of some BEING), and
then use the appropriate strategic knowledge to fill in that missing
program. The strategic knowledge will typically access and run many
other facet programs from many other concepts. In the course of
this, new concepts may be constructed and worth giving names to$$
If one part of a BEING becomes large and interesting, it may be split into
several brand new BEINGs. This is how new concepts develop. For
example, in filling out the Examples part of the BEING
dealing with Composition, the system will have to think up new compositions
and relations. If one of them turns out to be interesting, it will be
made into a new BEING, and almost all of its 25 parts will be blank. So the
system will then have 25 well-defined questions to try to answer about
a specific, promising new concept.
The Examples part of the Composition BEING would now contain a pointer to
this new BEING.*.
Whenever this happens, the new concept has almost all his facets
blank, which means AM now has about 20 specific tasks to eventually
attend to (if they're deemed interesting enough). So the system never
runs out of things to do; rather, that number keeps growing rapidly.
It is the judgmental criteria which must limit this otherwise-explosive
growth.
AM is interactive: AM informs a human user of the things it finds
which it thinks are interesting. The user can interrupt AM and
interrogate it, redirect its energies, and so on. Since the user has
several roles$$
Creator (decide what knowledge AM starts with), Guide (by encouragement,
discouragement, suggestion, hint), Absolute Authority (provide needed facts
which AM couldn't derive itself), Co-researcher (if AM is operating in a
domain unknown to the user). *,
AM should have several modes of communicating with him.$$
Traditional math
notation, textbook English, formal (e.g. AUTOMATH or predicate
calculus), pictorial (simulated visual intuitions), examples (I/O pairs, traces).*
Protocols indicate this is feasable; one should
only require a few minutes' instruction before
comfortably using the system.
The system will justify what it believes with ⊗4intuition⊗* and ⊗4empirical
evidence⊗* as well as with formal reasoning. This justification
would be recomputed only when needed (e.g., if an apparent
contradiction arose).
Intuition will be simulated by functions which are opaque$$ Their knowledge is
not inspectable by the rest of the system; e.g., compiled code * and fallible.
Below is a brief example of how they might work.$$ Consider the intuition about
a seesaw. This is useful for visualizing anti-symmetry and symmetry,
associativity, and the concept of multiplication (distance x weight).
Our seesaw function will accept some features of a seesaw scenario:
details about each person involved in the scene (exactly where they were,
what their names were, how much they weighed) and about the initial and final
position of the seesaw board. The intuition function SEESAW
would accept a ↓_partial_↓ list of such
features, and then return a fully-filled out list. If the final position of
the seesaw
is one of the omitted parameters,
the function will compute the sums of (weight x distance)
on each side, and decide what happened to the board. If some feature like a person's
name was omitted, it will fill that in by randomly choosing some name. Of course,
the caller of the function doesn't know which features are irrelevant; he doesn't
know which details of the gestalt are computed and which are random. *
.XGENLINES←XGENLINES-3
.NSECP(Details: Getting AM going)
This diversion is only for the interested reader. It may be skipped without
loss of continuity. It deals with short-cuts which can be taken by myself
to get AM running faster and more easily.
When AM proposes a conjecture, the user may interrupt and say "Assume it is true,
and go on". If he does this consistently, we can debug AM's higher-level
proposing abilities even before its lower-level proving abilities are perfected.
We may be able to beat the "critical mass" constraint slightly.
The vast amount of necessary initial knowledge can be
generated from a much smaller
core of intuition and definite facts, using the same collection of
strategies and wisdom which also drive the later discovery and the
development.
Since AM has been given good knowledge-acquisition (strategic) powers,
AM itself should be able to fill in the blank parts of the concepts it starts
with.$$
When you are preparing the knowledge to initially get AM going,
the way to save some effort is by
omitting whole categories of knowledge which you can expect
the system to discover quickly for itself.
AM has to have good methods for generating examples of whatever
concepts it later comes up with; those same methods can be used to produce
examples of the initially-supplied concepts. This means that the creators can
omit all examples of the concepts originally supplied; the system
will be able to fill in all such gaps.
Notice that AM has to be able to fill in ↓_all_↓ the parts (slots)
of each newly discovered concept, so perhaps only the barest definition or
intuition need be initially taught about each concept.*
The only constraint on
such a partially-equipped
system is that it first develop a broad base of
intuition, examples, and interrelations, spanning several areas of interest,
before trying to develop any one particular area in depth.
.XGENLINES←XGENLINES-2
There are two kinds of discovery, evolution of abilities, which are specifically
disallowed: (i) the modification of the strategies and
control mechanism themselves$$
This was decided against because our thesis is that the same strategies
useful for dealing with premathematical concepts should suffice no matter how
far the system progresses. One mechanism to effect this kind of development
is the standard sort of feedback paradigm, which in AM's case seems
one full step too ambitious *,
and (ii) the introduction of brand new ⊗4kinds⊗* of
questions, of new parts of a type not forseen at time of system creation.$$
The postulating of new kinds of parts is a very tricky process, and like the
first exclusion, I feel that the kinds of things one wants to know about
a concept shouldn't vary too much. A mechanism for introducing new kinds of
BEING parts is the following:
whenever a very interesting property P is discovered, with interesting variations,
which applies to many BEINGs, then assert that P is a new
part (slot, question), and that every BEING which has some variation of
this property should fill
in a slot labelled P, with a description of its variation.
The common link between all the
BEINGs having property P should be found, and any new BEING possessing this
characteristic should eventually try to see what variation of P it
possesses. That is, it should try to fill in a slot labelled P. *
.NSECP(Examples of Individual Modules)
Perhaps it would be beneficial to glance over the file GIVEN at this point.
Since that's a couple hundred pages long, we'll just glance at two
typical BEINGs: EXAMPLES and COMPOSITION.
Since the BEINGs are all considered equal, there is in fact no atypically
interesting one which can be exhibited. So the two below are just mediocre;
they aren't worth poring over.
.SSEC(The "EXAMPLE" module)
<Look at Examples BEING, from the Given file>
This is the BEING named ANY-BEING.EXAMPLES.
Notice the general hints listed here (.FILLIN) for filling in the examples
of any given concept. β is an abbreviation for BEING. Here (.CHECK) we see
how to check any unclear example, and (.REPR) here is the format to keep
each Examples part in. The Structure part says that we can split off any
interesting example into a new BEING with no bookkeeping required.
.BGIV
⊗2↓_EXAMPLES_↓⊗* {not} {bdy} Includes trivial, typical, and advanced cases of each type.
⊗1ACT GROUPING⊗*
FILLIN Specialize β (in various ways) until only one entity is specified.
Any kind: instantiate specializations, and/or defn, and/or intu.
Inefficient: scan related specific entities until an ex. is found
also: look for op. F: αα→β; then use f(αα.Examples).
Consider ana. β's examples, map them back. Examine similar β's exs.
Special: To get an example that satisfies P, bear P in mind at each spec. choice point.
Try setting various parameters s.t. they are equal to each other.
Simplest: plug in simple distinguished concepts into defn/intu. until singleton.
Consider the trivial case, the empty or minimal extreme, the base step of a recursive defn.
Big: Plug sophisticated, big, varied examples of each variable concept into defn/intu.
If recursive, try to invert it so as to be able to build up harder and harder exs.
Done: only use it to find a few actual examples.
Save the inverted procedure for later usage, though.
Pick some decent example, find a chain of simpler and simpler examples
leading backward, then turn around and extrapolate off the hard end.
Prototypical: so representative that they will be useful in the future for
testing a conjecture for empirical plausibility.
Potentially: formally prove that any tie to this ex. is a valid tie.
Boundary: keep an eye out for two similar examples, one in and the other out.
(these can come from work on this part and/or from similar B's exs.)
When such a pair is found, begin transforming them into each other,
and zero in on the most similar pair of in/out entities. Examine carefully.
Afterwards: if ¬∃ exs. before, ∃ exs. now, ∃ op O on β with no O.Exs, then
place into O.Exs. this suggestion: can plug eles. of β.Exs into O.
STRUCTURE Split off any indiv. or class of high-int. examples, keep the rest here.
CHECK Each ex. should satisfy the defn. and intu parts.
If any type of new procedure (e.g., inverted recursive defn) has been created,
which supposedly generates β's, try to conjecture about the uniqueness of the
members of the sequence produced, the totality of their covering of all possible β's, etc.
REPRESENTATION (name, type, (part present, value, change from β)*, origin, complexity,
distance from the boundary of β)*
Data about examples should be stored under part headings (easy to make them BEINGs).
The types of type are: +, + boundary, -, - boundary.
The types of origin are: by specializing defn, by intu, to satisfy property.
⊗1INFO GROUPING⊗*
DEFINITION Specific entities which are (not)(barely) instances of β's.
INTU Zero in on specific representatives, individuals.
EXAMPLES Access the Examples part of any BEING, and it contains examples of that.
TIES Up: Info group. Side: Specializations.
.END
.GROUP SKIP 2
.SSEC(The "COMPOSE" module)
<Look at Compose BEING, from the Given file>
RECOG:Here are productions which might match against the current situation.
INTEREST: Here are some special features that make a composition interesting.
Since composition is a type of operation which is a type of activity, these are
all in addition to (or exceptions to) the hints listed under
OPERATION.INTEREST and ACTIVITY.INTEREST and ANY-BEING.INTEREST.
VIEWS: Here is how to view this as a set, an operator, a relation, a property.
INTU: This specifies that we may abstractly manipulate expressions about
compositions by thinking in terms of arrows landing and being refired again.
This meshes with the intuition of an OPERATION as a set of arrows being fired
from one set into another.
.BGIV
⊗2↓_COMPOSITION_↓⊗* Apply an operation to the result of a previous operation.
⊗1RECOGNITION GROUPING⊗*
CHANGES {(eles. of dom. of 1st changed to some eles. of range of 2nd., .90, .80, )}
FINAL {(2nd range ele., .20, .70, intu: final product of a 2-step manufac. process)}
PAST
IDEN {not}{quick} This must be filled in for AM initially, but hasn't been yet.
⊗1ALTER GROUPING⊗*
GENERALIZATIONS Sequence of actions, an ordered pair of operations to perform.
FILLIN: Increase 1st true domain, typically by modifying the definition.
Increase 2nd range.
SPECIALIZATIONS Given an Active F:AxB→C, and an Active G:CxD→E, consider the new Active
h:(AxB)xD→E, written g*(fxi), defined as h((a,b),c)= g(f((a,b)),c). Alternatively,
given f:BxD→C and g:AxC→E, construct h:(AxB)xD→E as h((a,b),c)= g(a,f((b,c))).
An even further specialization: let some of A,B,C,D,E coincide.
An even further specialization: let all of A,B,C,D,E coincide.
BOUNDARY {(second operation doesn't care what the result of the first was, sequenceing unnec))}
DOMAIN/RANGE {not} (AOP↑2, OP, op)
FILLIN: domain is a pair of operations, range is a new operation whose domain
is the dom. of the 1st pair element, and whose range is the range of the 2nd.
int. depends on the 2 ops and on props which this particular op possesses;
if high enough and no ptr, BEINGize this new op.
ORDERING(Complete)
WORTH (.8, .95, .5, .5, .6, .9, .5, (1.0 formal, .8 intu), .8, (1.0 basis))
FILLIN: To forestall an infinite regress, decrease the activation energy of this investigation.
INTEREST Int. property of result which is not true of either argument relation.
Int. properties of both argument relations are preserved, undesirable ones lost.
Int. subsets (cases) of domain of 1st map into interesting subsets of range of 2nd.
Preimages of int subsets (cases) of range(2nd) are themselves interesting subsets of domain(1st).
The range of the first is equal to, not just a subset of, the domain of the second.
OPERATIONS
⊗1ACT GROUPING⊗*
BOUNDARY-OPERATIONS {not}
ALGORITHMS
FILLIN: Sequence: do 1st op (ALG), then take result and do 2nd op on it (ALG).
REPRESENTATION repr. as any operation, or perhaps just as 2nd o 1st.
VIEWS to view as a reln: view each arg. op. as a reln, R↓1 ⊂ AxB, R↓2 ⊂ BxC, composition
is a relation R↓2 o R↓1 ⊂ AxC, where (a,c) is in composition iff
(a,b) ε R↓1 and (b,c) ε R↓2.
to view as op: domain is dom of 1st, intermed. activity, then range is range of 2nd.
to view as a prop: prop. master set is (same notation) AxC; R↓2oR↓1(a,c)) ↔
R↓2(R↓1(a), c).
to view as a set: set of ordred pairs which is a subset of dom↓1 x range↓2.
⊗1INFO GROUPING⊗*
DEFINITION The sequencing of two operations, f and g, where domain of f contains the
range of g as a subset. E.g., f:A→D, and g:W→B with B⊂A.
Then the new combined operation is the composition of f and g, written
f o g, f(g), fg. The computation is straightforward; apply g and then apply
f to the result.
If f:AxB→C, g:D→A, and h:E→B, then one can consider the composition f o gxh,
also written f(g,h), whose value on (x,y) ε DxE is f(g(x),h(y)) ε C.
This is combinatorially explosive. Suggestions for containment: possibility of
considering f o gxg; f o ixj where at least one of i,j is the identity,
especially if the other one of i,j is equal to f itself; f o ixj, where one
of i,j is f, occasionally both are f. In general, f o gxh is about as intersting
as the ties between the three functions are already (equality is quite high).
To expand this flexibility, view any Active as an operation for these purposes.
The composition FoG is more formally defined as the specific set of ordered pairs
(a,B) where aεdom(G) and B⊂range(F), and B={F(c) | cεG(a)}, together with an
explicit statement of the domain and range of F and of G.
INTU Arrows emanate from one set, go into another set, new arrows go from there to
a third set. The composition means follow along and transfer to new arrows.
TIES Up: Operation
EXAMPLES {not} {bdy}
CONTENTS
.END
.NSECP(Example: The Modules Interacting)
Let's look at an example of a session with the system (the way AM ought to eventually
appear). Later,
we'll re-analyze this session to see just how AM managed it.
.SSEC(Some Early Numerical Concepts)
In order to be interesting, the example session takes place after AM has learned
a few numerical concepts. To make this more plausible, let me briefly show how some
of these might be discovered "naturally" by AM.
One of the things AM knows about relations is when they are interesting.
(The facet named "Interestingness" on the concept named "Relation".)
These
features include: (i) If R is a relation from A to B, then R is interesting if
the image of each element ⊗6xεA⊗* satisfies some B-interesting property; or,
(ii) all (x,y) pairs, for ⊗6x,yεA⊗*, are in some B-interesting relation.
Suppose we now consider relations from sets to sets, so A and B are two sets.
Then
SET.INTEREST is accessed, and he tells the system that
some interesting set properties and relations are known to be: singleton,
equal, disjoint. These lead, respectively, to the concepts of
Function (all images are singletons), Constant (all images are equal),
1-1 (no two images intersect).
.ONCE TURN OFF "-"
As another example, a composition is known to be interesting if its component
relations are, and if its domain and range are related by an interesting relation.
This leads to considering MAP-STRUCTURE(REVERSE-ORDERED-PAIR); that is, take
a relation, view it as a set of ordered pairs, then reverse each one, then
view the resultant set as a relation again.
This is just the concept of Inverse, and is interesting because it takes
relations on CROSS-PRODUCT(A,B) into relations on CROSS-PRODUCT(REVERSE((A,B)).
For our example, all the following concepts should be developed already;
if any are improbable, tell me and I will present some natural scenario for
their discovery:
Count$$ This operation converts any list (of length n)
into canonical form (perhaps a list of n NILs).*,
Inverse, Commutativity, Transitivity, Associativity, Singleton, Function,
Successor, Zero, Plus, Times, One, Two.
.SSEC(A Hypothetical Session)
Assume that AM has a grasp of the early numerical concepts mentioned, as well
as of premathematical ones.
We are now ready to examine the
example of how a session with AM might appear to the user.
In a few minutes,
we'll go into detail about how AM actually does this.
Suppose that AM has just considered repeated TIMES-ing, that is, exponentiation.
<THE FOLLOWING IS THE COMPLETE SLIDE; AFTERWARDS IS THE SET OF ACCOMPANYING PATTER>
.BEGIN SELECT 6 FAS INDENT 0,3,0
1. SYSTEM: Rate of drop of interest in Repeated TIMES-ing
(compared to SUCCESSOR, PLUS, TIMES) is huge.
Not associative or commutative; no Left identity element.
Dissuades me from pursuing higher order constructed operations.
2. SYSTEM: I am now investigating the inverses of Plus and Times.
In general,
the inverses
are not functions.
3. SYSTEM: Looking at more examples of TIMES⊗A-1⊗*.
TIMES⊗A-1⊗*(n) seems always to include, as one ordered pair,
(n, 1). Same for (1, n).
Conjecture: (∀xεN) (x,1) ε TIMES⊗A-1⊗*(x), and (1,x) ε TIMES⊗A-1⊗*(x).
4. SYSTEM: Proof is simple: TIMES(x,1)=x=TIMES(1,x).
5. SYSTEM: The two pairs (n,1) and (1,n)
are distinct iff the number n is not equal to 1.
Noticing the number 1 as an exception, we can state:
Corollary: COUNT*TIMES⊗A-1⊗*(1) = 1; (∀x>1) COUNT*TIMES⊗A-1⊗*(x) ≥ 2.
COUNT * TIMES⊗A-1⊗* is the how many ways one may express a number as a product
of an ordered pair of numbers.
6. SYSTEM: Interesting to consider the subset P of N,
defined as {xεN | COUNT*TIMES⊗A-1⊗*(x)=2}.
7. USER: (interrupting) Why is this interesting?
8. SYSTEM: At the moment, we have the known fact f(x)≥y; try to pin down extreme cases,
those x for which f(x) is precisely equal to y. f is COUNT*TIMES⊗A-1⊗*, in the current
case, and y is 2. Do you have any special names you would like me to refer to
COUNT * TIMES⊗A-1⊗* by? Any special names for the subset P?
9. USER: Call that composition FAC.
Call the set P, of extreme numbers under FAC, PRIMES.
10. SYSTEM: Syntactic transformation: PRIME is the predicate which means "is in PRIMES".
11. SYSTEM: TIMES may also be viewed as operating on a BAG;
in this sense, TIMES⊗A-1⊗* would
return all possible bags (of any length) whose product is the given number.
We do not allow bags to have <2 members, and we do not allow bags longer than 2
to have any 1's in them.
In this case, (5) just says: COUNT(TIMES⊗A-1⊗*(x)) ≥ 1.
The extremes now are just 1 and PRIMES.
I want a new name for this new interpretation of TIMES⊗A-1⊗*.
12. USER: Call it FACTORS.
13. SYSTEM: Conjecture: FACTORS(x) always seems to contain a bag containing only
ones and primes, and only one such bag.
14. SYSTEM: Proof of existence is by contradiction,
using the lemma ¬PRIME(x) → ∃(u,v)εTIMES⊗A-1⊗*(x) s.t. 1<u<x, 1<v<x.
Proof of Uniqueness is by contradiction, using the lemma
(∀a,bεN, xεPRIMES). x|TIMES(a,b) iff x|a or x|b.
15. USER: Call this the unique factorization theorem. This is very important.
Consider now the sum of all the divisors of a number.
16. SYSTEM: PLUS * UNION * TIMES⊗A-1⊗* is being investigated. Seems to range from
a low extreme of Successor(the number) up to a high extreme of almost
Times(the number, itself). The numbers at the low extreme seem to be the primes.
The numbers near the high extreme may not be worth naming. An intermediate point
is twice the number itself.
That is, those numbers n s.t. Times(2,n)= PLUS*UNION*TIMES⊗A-1⊗*(n).
Another intermediate set of points is PRIMES;
that is, those numbers n s.t. PRIME(PLUS*UNION*TIMES⊗A-1⊗*(n)) holds.
This may lead to the conjecture that P*U*T(N) = PRIMES.
17. USER: Call these =2n numbers "Perfect Numbers." Call the others nothing.
There are not many interesting things to prove involving either idea.
18. SYSTEM: Going on to new topic, then. I shall
consider comparing TIMES⊗A-1⊗* collections from two numbers.
<this leads to GCD and relative primeness>
.END
.SSEC(Comments on the Session)
.BEGIN SELECT 6 FAS INDENT 0,3,0
1. AM is not thrilled with exponentiation, so it doesn't even
consider the hyper-(repeated-)exponentiation operation.
2. SYSTEM: I am now investigating the inverses of Plus and Times.
In general, the inverses are not functions.
3. AM notices that (x,1) and (1,x) are always allowed factorizations of x.
5. A corollary is that TIMES⊗A-1⊗* has at least two members.
6. AM now decides to consider just those numbers whose
TIMES⊗A-1⊗* has ⊗4precisely⊗* 2 members.
7. The user asks why this is interesting.
8. SYSTEM: At the moment, we have the known fact f(x)≥y; try to pin down extreme cases,
those x for which f(x) is precisely equal to y. f is COUNT*TIMES⊗A-1⊗*, in the current
case, and y is 2. Do you have any special names you would like me to refer to
COUNT * TIMES⊗A-1⊗* by? Any special names for the subset P?
9. USER: Call that composition FAC, standing for "pairwise factorings".
Call the set P, of extreme numbers under FAC, PRIMES.
11. AM notices that TIMES may also be viewed as operating on a MULTISET.
In this sense, TIMES⊗A-1⊗* would
return all possible multisets (of any length) whose product is the given number.
In this case, (5) just says that TIMES⊗A-1⊗*(x) has at least one member.
The extremes now are just 1 and PRIMES.
AM requests a new name for this new interpretation of TIMES⊗A-1⊗*.
12. USER: Call it FACTORS.
13. SYSTEM: Conjecture: FACTORS(x) always seems to contain a bag containing only
ones and primes, and only one such bag.
14. AM proves both existence and uniqueness by contradiction,
using the two lemmas it devises.
15. USER: Call this the unique factorization theorem. This is very important.
Consider now the sum of all the divisors of a number.
This leads AM to devise PERFECT NUMBERS.
.END
.SSEC(The Session Revisited: An In-Depth Example)
.TURN OFF "{}"
.SSSEC(The control structure reviewed)
Before examining how AM "really" could carry on the hypothetical dialogue,
let's review the global control structure of the system.
The basic process is to repeatedly (i) see which part of which BEING
is most relevant (w.r.t. CS, the current situation),
then (ii) deal with that part of that BEING (either
⊗4execute⊗* it, or try to fill it in more). Often, new entities are
constructed$$ E.g., when filling in the EXAMPLES slot of some BEING *.
When this happens, they are evaluated for
interestingness. Any new, promising construct is temporarily
given full "BEING" status:
we assume that all 25 parts might be worth filling in;
we try to answer all 25 "questions" for this new concept.
After a while, if it
doesn't prove interesting, we "forget" this BEING.$$ Perhaps we
replace it as one subpart of one slot of one BEING, where it came from. This is
also where it would have remained, if it had never seemed interesting. *
Say we are dealing with part P of BEING B, which we abbreviate B.P.
In the case of extending (or filling it in, if it is currently empty), AM simply
gathers together algorithms suitiable for filling in the slot named ⊗4<P or any
generalization of P>⊗* in the BEING named ⊗4<B or any generalization of B>⊗*.
One extreme
case of the latter generalization is
"algorithms for filling in slot P in ⊗4any⊗* BEING";
though general, this is probably the most common kind of strategy information.
The reason is that most of the information for how to find the answer to some
given facet of a concept does ⊗4not⊗* depend on the kind of concept so much as
the kind of facet.
One of these general packets of knowledge was the ANY-BEING.EXAMPLES BEING we looked at.
.SSSEC(Looking at the new concept named "FACTORS")
Let us now consider a fairly detailed example. We shall pick up near the
end of our earlier dialogue, and explain how AM studies the new BEING FACTORS,
notices the unique factorization theorem, and tries to prove it.
.BEGIN FAS
After the user gives this Active Operation BEING the new name "FACTORS",
it is so recorded.
The definition part of FACTORS is already filled in, namely
⊗6"FACTORS(x) ≡ {b | BAG(b) ∧ TIMES(b)=x ∧ 1¬εb}."⊗*
The intuition part already contains the adequate images of: partitioning a set
into disjoint subsets of equal size; dissection; looking more closely at an artifact
until it divides up into its constituent parts;
dividing up a pile of marbles into smaller piles which all balance each other.
The control function takes over. Recall it wants to repeatedly choose B and P, then
deal with part P of BEING B, abbreviated B.P.
.INDENT 0,3,0
1. Neither P nor B is known. Ask each BEING how relevant it is to the
current situation, CS. Since CS contains many references to the recently-named
FACTORS BEING, and since that BEING is still quite incomplete, it is not surprising
that it wins this contest. To decide which part of FACTORS to deal with,
and how, we look
at FACTORS.ORDERING; it doesn't exist yet. We next look at
(generalization FACTORS).Ordering; in this case,
FACTORS is a kind of OPERATION, so we look at
OPERATION.ORDERING.
This too is blank. Ultimately, we look at ANY-BEING.ORDERING, which has some
quite general hints for which order the parts should be dealt with. In particular,
"concentrate on filling in the General Information parts before doing anything else."
These in turn are ordered "definition, intuition, examples, ties."
The definition and intuition parts are nicely filled out already.
The Examples part is blank, however, and that is where
AM chooses to work now.
2. So AM has chosen B=FACTORS, P=EXAMPLES. AM is going to fill in the part
labelled FACTORS.EXAMPLES. The control system now goes about collecting relevant
algorithms (and constraints) from the parts labelled
[(generalization⊗A*⊗* FACTORS).(generalization⊗A*⊗* EXAMPLES)].FILLIN.
These parts are:
.BEGIN NOFILL TURN OFF "[]" TABS 32,62; TURN ON "\" INDENT 2
[FACTORS.Examples].Fillin\[FACTORS.Genl-Info].Fillin\[FACTORS.Any-Part].Fillin
[OPERATION.Examples].Fillin\[OPERATION.Genl-Info].Fillin\[OPERATION.Any-Part].Fillin
[ACTIVE.Examples].Fillin\[ACTIVE.Genl-Info].Fillin\[ACTIVE.Any-Part].Fillin
[ANY-BEING.Examples].Fillin\[ANY-BEING.Genl-Info].Fillin\[ANY-BEING.Any-Part].Fillin
.END
.ONCE PREFACE 0 INDENT 3
Of these 9 slots, only two have executable code:
[ANY-BEING.EXAMPLES].FILLIN contains almost a page of general techniques for
filling in examples. [ACTIVE.EXAMPLES].FILLIN has about half as many special-purpose
hints which apply whenever the entity is an Activity, ⊗4after⊗* the more general
techniques have been applied.
The control structure now simply appends these specific algorithms onto the
more general algorithms, and comes up with a little program to fill in
FACTORS.EXAMPLES. This program is run, with (FACTORS,EXAMPLES) as its arguments,
and then control will revert to the "select best B,P" phase.
.ONCE PREFACE 1 INDENT 0,6,0
<IF TIME IS SHORT:>
Time doesn't permit me to go through the whole assembled program. It calls for
manipulating the definition and intuition parts of FACTORS to obtain examples.
In fact, it manages to compute FACTORS of the numbers 0,1,2, and 75.
<POINT TO 12:> Here, after these have been computed, they are entered on
the FACTORS.EXAMPLES part. AM then looks at the OPERATIONS part of FACTORS,
and finds various activities listed. For each one of these, it consults its
EXAMPLES part. If it's incomplete, it leaves a little note there saying
"if you want examples of your domain elements, one sure place to find some is on
FACTORS.EXAMPLES." Here we see an instance of how adding knowledge to AM
makes later activity run faster, not slower.
<SKIP THE REST OF THIS SECTION; GO TO 6.2>
<IF TIME IS NOT SHORT:>
3. Let us now go through this assembled program, and see how it fills in examples
for the FACTORS concept. The first thing it says to try is
"for each specialization x of FACTORS, take all of x.EXAMPLES if it is filled in ;
if not, try to instantiate the description of x and thereby produce such an example".
But the Specializations part of FACTORS hasn't been filled in at all, so there is
no x to work with. A note is placed in FACTORS.SPECIALIZATIONS, which says:
when you get filled in, instantiate yourself into an example for FACTORS.EXAMPLES".
This concludes the first of about 30 tactics listed under ANY-BEING.EXAMPLES.FILLIN.
4. The second thing to try is "instantiate the definition of FACTORS".
The definition is:
⊗6"FACTORS(x) ≡ {b | BAG(b) ∧ TIMES(b)=x ∧ 1¬εb}."⊗*
To instantiate it, AM must find a specific number x and a set of bags {b},
satisfying
t↓u conditions. Since we know TIMES⊗A-1⊗*(2)={(1,2),(2,1)}, it is clear that
FACTORS(2) = {(BAG 2)}.
This is our first real example.
5. The next hint says "instantiate the intuition". Suppose we look at the
image "partition a set into disjoint subsets of equal size".
To instantiate it, take a specific
set, say {a,b,c,d,e,f}.
By enumeration, the only ways to do this are: one subset with 6 elements,
two subsets each with 3 elements, three subsets each with 2 elements, and
6 subsets each with 1 element. The intuition directs the translation of these
results into the statement that the only bags whose TIMES is 6 are:
(BAG 1 6), (BAG 2 3), (BAG 3 2), (BAG 6 1). Eliminating 1's and multiple
occurrences of the same bag, we can say FACTORS(6) = {(BAG 6),(BAG 2 3)}.
This is our second example.
6. The next thing to try is "find an analogy between FACTORS and some other
BEING, say x, and then try to map over the examples of x into examples of FACTORS."
There are no such analogies known at present, so this fails.
7. The next type of example to search for is coincidental: some of the variables in
the definition might coinicide. But the only variables here are x and b, one of
which is a number and the other a bag, so no coincidence is possible.
8. Search for the simplest possible examples. Plug the extreme cases of the domains
into the definition. Thus we ask the BEING named NUMBERS what his extreme examples
are. He replies "0 and 1". AM now tries to compute FACTORS(0). This means finding
a bag satisfying TIMES(b)=0. AM asks the BEING named TIMES if he knows any such
b's. TIMES.EXAMPLES replies Yes; in fact, ⊗4any⊗* bag b is allowed if it contains
a ZERO. Thus FACTORS(0) = ⊗6{b | BAG(b) ∧ 0εb ∧ 1¬εb}⊗*.
Finding FACTORS(1) again involves asking TIMES, who says that the only bags whose
image under TIMES is 1 are those consisting only of ONE's. But there is no bag
of 1's not containing a 1, except for the empty bag. So FACTORS(1)={(BAG)}.
9. Search for a sophisticated, huge example. Plug in a sophisticated case of the
argument of FACTORS. AM asks NUMBER.EXAMPLES for a big example, and gets back
(in canonical form) the number 75. After much trial and error, this is finally
converted into the example:
FACTORS(75)={(BAG 3 5 5), (BAG 75), (BAG 5 15), (BAG 3 25)}.
10. No prototypical example can be found, because so little is known about FACTORS.
11. No boundary examples can be found, since the concepts involved don't have meaningful
boundary examples.
12. At this point, our assembled program tells us to insert a mesage into each
slot of the form <member of FACTORS.OPERATIONS>.EXAMPLES, saying "if you want
examples of your domain elements, one sure place to find some is on FACTORS.EXAMPLES".
Here we see an example of how adding knowledge to AM will make later processing
⊗4shorter⊗*, not longer: forestalling a future search by leaving the proper information
in a place where it will be found immediately -- but only -- when later needed.
13. That was the final hint taken from [ANY-BEING.EXAMPLES].FILLIN; AM now turns
to those on [ACTIVE.EXAMPLES].FILLIN.
None of these turns out to be applicable here, so the assembled program is finished,
AM has dealt with FACTORS.EXAMPLES, and control reverts to choosing which B,P to
deal with next.
.SSSEC(Conjecturing the Unique Factorization Theorem)
THE CONJECTURING PROCESS: abbreviated
(See commentary immediately following the abbreviation)
.BEGIN SELECT 6 FILL SINGLE SPACE PREFACE 1 INDENT 0,3,0 TURN OFF "{}-"
1. Choose B=FACTORS, P=TIES.
Gather relevant algorithms from the slots labelled:
[FACTORS.Ties].Fillin, [FACTORS.Genl-Info].Fillin, [FACTORS.Any-Part].Fillin,
[OPERATION.Ties].Fillin, [OPERATION.Genl-Info].Fillin, [OPERATION.Any-Part].Fillin,
[ACTIVE.Ties].Fillin, [ACTIVE.Genl-Info].Fillin, [ACTIVE.Any-Part].Fillin,
[ANY-BEING.Ties].Fillin, [ANY-BEING.Genl-Info].Fillin, [ANY-BEING.Any-Part].Fillin.
2. "Let D be the
known BEING representing
the kind of entity in the
range of FACTORS. Then ask D.INTEREST how to look for interesting
properties or regularities. If sparse, ask (generalization⊗A*⊗* D).INTEREST also.
Apply these methods to the output of a typical example of FACTORS.
Check interesting property found, by seeing if it holds
for the other outputs from FACTORS and ensuring it isn't simply part of the
definition of FACTORS."
3. Ask SET.INTEREST and STRUCTURE.INTEREST for perceptual guidance about
a particular output,
say the output
{(BAG 3 5 5) (BAG 75) (BAG 5 15) (BAG 3 25)} from the call FACTORS(75).
4. "Three
distinct ways a structure S can be interesting:
S satisfies a known interesting property of Type(S).
Every xεS satisfies
some single,interesting property.
⊗4Some⊗* xεS
satisfies some very interesting property."
5. First and second hints fail.
Now look at each element in turn, that is, each
bag. First consider (BAG 75). This satisfies the property SINGLETON.
Checks with other examples of FACTORS.
Conjecture:
∀x.(BAG x)εFACTORS(x).
6.
Look at (BAG 3 5 5). Each element satisfies PRIME.
All other examples of FACTORS check.
Conjec: FACTORS(x) always contains a bag of primes.
7.
Look at (BAG 3 5 5) still.
Each element satisfies ODD. Does not check out:
FACTORS(2) = {(BAG 2)}.
8. Look at (BAG 5 15) and at
(BAG 3 25). Nothing interesting.
9. Jumping ahead:
⊗6PF(x) = FACTORS(x) ∩ MAPSTRUC(PRIME, x) = {b | BAG(b) ∧ TIMES(b)=x ∧ 1¬εb ∧
∀zεb. PRIME(z)}⊗*.
Conjecture: PF is a function.
.END
COMMENTARY on the Conjecturing abbreviation
0. A special heuristic, embedded immutably in the control structure, has
AM make a slight effort to deal with the same B ⊗4or⊗* P as it did last
time, but not the same B.P of course. It is not surprising then that
FACTORS is again selected; this time, the TIES part is chosen to be filled in.
So AM is looking for some conjectures involving the concept FACTORS.
1. Information is gathered as before; this time, the relevant parts are:
.BEGIN NOFILL TURN OFF "[]" TABS 33,63; TURN ON "\" INDENT 3
[FACTORS.Ties].Fillin\[FACTORS.Genl-Info].Fillin\[FACTORS.Any-Part].Fillin
[OPERATION.Ties].Fillin\[OPERATION.Genl-Info].Fillin\[OPERATION.Any-Part].Fillin
[ACTIVE.Ties].Fillin\[ACTIVE.Genl-Info].Fillin\[ACTIVE.Any-Part].Fillin
[ANY-BEING.Ties].Fillin\[ANY-BEING.Genl-Info].Fillin\[ANY-BEING.Any-Part].Fillin
.END
2. just read through
3. Because the output of a call on FACTORS is a ⊗4set⊗* of bags,
we are directed to ask SET.INTEREST for aid
in perceiving interesting things about a particular output,
say the output
{(BAG 3 5 5) (BAG 75) (BAG 5 15) (BAG 3 25)} from the call FACTORS(75).
SET.INTEREST is not very big, so we ask STRUCTURE.INTEREST as well.
4. STRUCTURE.INTEREST explains that there are three
distinct ways a structure can be interesting.
First, check whether the structure satisfies any known interesting property of that
type of structure.
If not, check to see whether every element satisfies
the same interesting property. If not, check to see if ⊗4some⊗* element of the
structure satisfies some very interesting property.
The criteria for interestingness being talked about here is the one specified
by the BEING representing the type of the elements. In our present case,
our set is a set of ⊗4bags,⊗* so that
means consult all the hints and factors present under BAG.INTEREST. But this is
also very sparse, hence we recursively turn to
STRUCTURE.INTEREST for evaluation criteria.
5. After a reasonable time, AM cannot find any interesting property satisfied by the
given output set.
It also fails to find any single interesting property satisfied
by all four bags which form the elements of that output set.
Now AM looks at each element in turn, that is, each
bag. First we consider (BAG 75), say. This satisfies the property SINGLETON.
We check with other examples of FACTORS and, sure enough, each one of them
contains, as an element, a bag having the property SINGLETON. Comparing these
singletons to the inputs to FACTORS, we conjecture that
(BAG x) will always appear in the output set of FACTORS(x).
6. We go back to looking at the individual bags in FACTORS(75).
This time we
look at (BAG 3 5 5). Each element ⊗4does⊗* satisfy an interesting property,
namely PRIME. We check against the other examples of FACTORS, and sure enough
each one of them contains an element which is a bag of primes. There doesn't
seem to be any obvious relationship to the input argument, so we merely
conjecture that FACTORS(x) always contains a bag of primes, without saying
which primes or how to compute them. This is one half of the Unique Factorization
Theorem. Notice that this is "rough around the edges", namely for the cases
of factors of zero and one, but these will be caught later by an expert BEING
who specializes in checking conjectures just before we start to prove them.
7. Each element of (BAG 3 5 5) also satisfies the property ODD. But this is quickly
rejected by looking at the example FACTORS(2) = {(BAG 2)}.
8. We now look at the next individual bag in FACTORS(75), namely (BAG 5 15).
Nothing interesting is found here or in the next case, (BAG 3 25).
9. Before going on to prove some of these conjectures, let's see how AM might
notice the uniqueness aspects of them. AM knows that some elements of FACTORS(x)
satisfy MAPSTRUC(PRIME), but some don't. It wants to find out how to characterize
those which do; namely, those bags of primes from those containing a nonprime.
So AM will temporarily create a new BEING, called say PF, defined as
⊗6PF(x) = FACTORS(x) ∩ MAPSTRUC(PRIME, x) = {b | BAG(b) ∧ TIMES(b)=x ∧ 1¬εb ∧
∀zεb. PRIME(z)}⊗*.
Which means: all bags of primes whose TIMES is x; which also means all
factorizations of x into bags containing only primes.
In a manner similar to the above, AM will notice that PF of each number seems to
be a SINGLETON. That is, there is only one bag of primes in the FACTORS(x) collection
for a given x.
The unique factorization theorem can now be
consisely be stated as "PF is a function defined on N".
In such a form, it is not surprising that AM will routinely investigate it.
.SSSEC(Proving Existence)
THE PROVING PROCESS abbreviated
(See commentary immediately following the abbreviation)
.BEGIN SELECT 6 FILL SINGLE SPACE PREFACE 1 INDENT 0,3,0 TURN OFF "{}-"
1. B = UFT, P= Justification.
2.
[ANY-BEING.JUSTIFICATION].FILLIN
says to execute
GUESS.ALGORITHMS and PROVE.ALGORITHMS.
3.
"Supporting Contacts".
Test UFT on extreme cases.
Means select a number x, then comput FACTORS(x), then check
that one of the bags so produced consists purely of primes.
NUMBER says
that the extremes are 0, 1, and sometimes 2. Failure of 0,1.
Modify the wording of UFT:
⊗6∀numbers x>1, ∃ bag bεFACTORS(x) s.t. ∀zεb.PRIME(z).⊗*
4. PROVE.ALGORITHMS passes off to
Math-Induction.ALGORITHMS.
Base case x=2; constructor SUCCESSOR.
Base case already solved.
5. Assume UFT for all number between 2 and x.
Problem: prove
UFT(SUCCESSOR(x)).
Not trivial transformation.
Intuition indicates: proof by cases, where cases are:
SUCCESSOR(x) is/isn't prime.
6.
Assume x+1 is a prime.
Lemma: ⊗6∀x>2,(BAG x)εFACTORS(x).⊗*
7.
Assume x+1 is not prime.
Write x+1 as TIMES(u,v),
where both u and v are between 1 and x+1.
Work backwards; Lemma:
For any number a, bag b of numbers, bag d of numbers, if a=TIMES(b) and aεd,
then TIMES(d) = TIMES( SUBSTITUTE(b for a in d)).
8. Proofs of the two lemmas...
.END
COMMENTARY on the Proving abbreviation
There are many good automated theorem provers around, many of them embodying
some of the heuristics that AM does. So it's probably not worth laboring on
through the proof of the UFT.
The interesting aspect of AM is that it ⊗4proposed⊗* the conjecture.
Let's just go a step into this, to see how AM cleans up the (slightly-incorrect)
statement of UFT which was proposed as a conjecture.
This conjecture is made into a temporary BEING,call it UFT, and eventaully AM gets around
to filling in its JUSTIFICATION part.
1. Skipping some of the details, assume that the control structure chooses to
work on filling in the JUSTIFICATION part of that new conjecture.
2. The plan for action is assembled
out of the nonblank slot labelled: [ANY-BEING.JUSTIFICATION].FILLIN, which in turn
directs our energies to following the activities specified by
GUESS.ALGORITHMS and PROVE.ALGORITHMS.
3. The only hint on GUESS.ALGORITHMS which affects UFT is the one called
"Supporting Contacts". It says that we should try to test the conjecture
on extreme cases. By asking UFT, we find that testing it in a specific
case means selecting a number x, then computing FACTORS(x), then checking
that one of the bags so produced consists purely of primes.
To find extreme cases means therefore to find extreme numbers. NUMBER says
that the extremes are 0, 1, and sometimes 2. Sure enough, zero and one fail
the UFT conjecture! The hint on GUESS.ALGORITHMS says that if only extreme
cases fail, to simply modify the statement of the conjecture to allow for these
exceptions. The definition of UFT now becomes:
⊗6∀numbers x>1, ∃ bag b of prime factors⊗*
4. We now execute the code found under PROVE.ALGORITHMS, with UFT as our argument.
This is where we shall leave our proof example.
<IF TIME IS SHORT, SKIP TO NEXT SECTION!!>
This sets up some demons to watch for places to declare lemmas, use intuition,
etc. Then each type of proof$$ Universal, Existential, Forward, Backward,
Direct, Indirect, Constructive, Nonconstructive, Mathematical Induction,... *
(which are themselves BEINGs) examine UFT to see how relevant they are.
The winner is, say, Proving-Universal-Statments (abbreviated Univ).
His ALGORITHMS part says to consider Mathematical Induction first.
The Math-Induction BEING's ALGORITHMS part says to clearly decide on the
base case and the constructor function. In the case of UFT, this is simply
the case x=2 and the function SUCCESSOR. A big boost in confidence occurs
when Math-Induction finds the base case has just been solved elsewhere
(UFT was verified for the case x=2 when we looked at the extremes 0,1,2).
5. The assumption now made is that UFT is true for x and all its predessors
(down to the number 2, though not below). The problem is now to prove that
UFT holds when x is replaced by SUCCESSOR(x), call it y.
After some effort, AM gives up trying to establish this in any trivial way.
The intuition for UFT should provide the hint that UFT would be true for y
either becuase y is a fundamental building block, or if not then
y must be built out of blocks much smaller than y.
This translates as a proof by cases, and PROOF-BY-CASES tries to run.
The two cases suggested by intuition are: SUCCESSOR(x) is/isn't prime.
6. The first of these subtasks is started by assuming that UFT is true for
2,3,...,x, and that x+1 is a prime. But the only conjecture that filling in
FACTORS.TIES provided, besides UFT, was the one saying that (BAG x) is
an element of FACTORS(x). So in our present case (BAG x+1) would be a singleton
bag, whose only element was a prime, and which was found in FACTORS(x+1).
Thus we set up, as a lemma, the fact that ⊗6∀x>2,(BAG x)εFACTORS(x).⊗*
7. The second subproblem is started by assuming that UFT is true for
2,3,..,x, and that x+1 is not a prime. Intuitively, that means that x+1 can
be split into two very small pieces, each much smaller than x, and hence for
whom UFT holds. One of the known properties of PRIME is that
⊗4not⊗* being prime lets you conclude that the number is the product of two
which are smaller but not as small as 1.
In the present case, noting that we again need to ensure x>1,
we are thus able to write x+1 as TIMES(u,v),
where both u and v are between 1 and x+1.
To use this fact, we must work backwards and observe that what we need is
the lemma:
For any number a, bag b of numbers, bag d of numbers, if a=TIMES(b) and aεd,
then TIMES(d) = TIMES( SUBSTITUTE(b for a in d)).
Thus we can express x+1 as TIMES((BAG u v)), but by the inductive hypothesis
u=TIMES(r) and v=TIMES(s), for some two bags of primes r,s. By the lemma,
we can replace u and v by the elements of r and s, get a new large bag of primes,
and TIMES applied to this large bag is still x+1.
8. The two lemmas used in this proof are set up as new BEINGs, and their justifications
will eventually be attended to. The first one is proved so easily that it is not
even mentioned to the user; the second one is interesting in its own right as well
as longer to prove, hence it is mentioned and remembered. The proofs of these
lemmas, and the proof of the uniqueness half of the UFT, will be omitted here.
Notice that in all this processing, just a few lines have been printed out to the
user, and there has been no guidance from him whatsoever.
.END
.NSECP(Timetable and Size of AM)
.BEGIN NOFILL INDENT 0 PREFACE 0 TABS 45,55 TURN ON "\" SELECT 1
.SSEC(Parameters Characterizing the Magnitude of AM)
NUMBER\Initially\Ultimately
\\ but recall: there is no set goal
Number of Families of BEINGs\ 5\ 5
Number of BEINGs per family\ 30\100
Number of Parts per BEING\ 25\ 25
Size of each part (lines of LISP)\ 5\ 7
Number of parts filled in\ 8\ 20
Size of avg. BEING (LISP lines)\ 40\140
Total number of BEINGs\150\500
Core used by AM\200K\500K
Time per int. result (cpu min)\ 15\ 5
CPU time used (hours)\ 0\ 50
Human time used (person-hours)\300\1500
Dissertations completed\ 0\ 1
.E
.SSEC(Timetable for the AM Project)
(i). Codify the necessary core of initial knowledge
(facts and the wisdom to employ them).
⊗7Reality: See Given Knowledge, as presented in a separate volume.
Completed in December, 1974.⊗*
.BEGIN TURN ON "{"
(ii). Formulate a sufficient set of new ideas,
design decisions, and intuitive assumptions
to make the task meaninful and feasable.
⊗7Reality: firmed up in January, 1975.⊗*
(iii). Use these ideas to represent the core knowledge of mathematics collected
in (i),
in a concrete, simulated system.
⊗7Reality: the current version of Given Knowledge casts this into the concept-family format.
Hand-simulations done during February and March, 1975, with this "paper" system.⊗*
(iv). Implement a realization of AM as a computer program.
⊗7Reality: Under way in April, 1975.⊗*
(v). Debug and run the system. Add the natural language abilities gradually, as needed.
⊗7Reality: Scheduled for May to November of 1975. First interesting results
expected in late June.⊗*
(vi). Analyze the results obtained from AM, with an eye toward: overall
feasability of automating creative mathematical discovery and theory development;
adequacy of the initial
core of knowledge; adequacy of the ideas, design decisions, implementation
details, and theoretical assumptions. Use the results to improve the system;
when "adequate," forge ahead as far as possible into as many domains as possible,
then reanalyze. ⊗7Reality:
the (v)↔(vi) cycle will terminate in the Winter of 1976.⊗*
(vii). Experiment with AM. ⊗7Reality: scheduled to begin in December, 1975.⊗*
.END
.ASEC(Bibliography)
All the references below have actually been read as background for AM.
They form what I hope is a comprehensive list of publications dealing
with automated theory formation and with how mathematicians do research.$$
From a single author or project (e.g., DENDRAL), only one or two
recent papers will be listed.*
I strongly recommend those with an "α@" sign; the others proved to be merely
supplementary.
.ASSEC(Books and Memos)
.BEGIN FILL SINGLE SPACE PREFACE 1 INDENT 0,4,0 TURN OFF "@"
Adams, James L., zz4Conceptual Blockbusting⊗*, W.H. Freeman and Co.,
San Francisco, 1974.
Allendoerfer, Carl B., and Oakley, Cletis O., ⊗4Principles of
Mathematics⊗*, Third Edition, McGraw-Hill, New York, 1969.
Alexander, Stephen, ⊗4On the Fundamental Principles of Mathematics⊗*,
B. L. Hamlen, New Haven, 1849.
Aschenbrenner, Karl, ⊗4The Concepts of Value⊗*, D. Reidel Publishing
Company, Dordrecht, Holland, 1971.
Atkin, A. O. L., and Birch, B. J., eds., ⊗4Computers in Number Theory⊗*,
Proceedings of the 1969 SRCA Oxford Symposium, Academic Press, New York,
1971.
Avey, Albert E., ⊗4The Function and Forms of Thought⊗*, Henry Holt and
Company, New York, 1927.
@Badre, Nagib A., ⊗4Computer Learning From English Text⊗*, Memorandum
No. ERL-M372, Electronics Research Laboratory, UCB, December 20, 1972.
Also summarized in ⊗4CLET -- A Computer Program that Learns Arithmetic
from an Elementary Textbook⊗*, IBM Research Report RC 4235, February
21, 1973.
Bahm, A. J., ⊗4Types of Intuition⊗*, University of New Mexico Press,
Albuquerque, New Mexico, 1960.
Banks, J. Houston, ⊗4Elementary-School Mathematics⊗*, Allyn and Bacon,
Boston, 1966.
Berkeley, Edmund C., ⊗4A Guide to Mathematics for the Intelligent
Nonmathematician⊗*, Simon and Schuster, New York, 1966.
Berkeley, Hastings, ⊗4Mysticism in Modern Mathematics⊗*, Oxford U. Press,
London, 1910.
Beth, Evert W., and Piaget, Jean, ⊗4Mathematical Epistemology and
Psychology⊗*, Gordon and Breach, New York, 1966.
Black, Max, ⊗4Margins of Precision⊗*, Cornell University Press,
Ithaca, New York, 1970.
Blackburn, Simon, ⊗4Reason and Prediction⊗*, Cambridge University Press,
Cambridge, 1973.
@Brotz, Douglas K., ⊗4Embedding Heuristic Problem Solving Methods in a
Mechanical Theorem Prover⊗*, dissertation published as Stanford Computer
Science Report STAN-CS-74-443, AUgust, 1974.
Bruner, Jerome S., Goodnow, J. J., and Austin, G. A., ⊗4A Study of
Thinking⊗*, Harvard Cognition Project, John Wiley & Sons,
New York, 1956.
Charosh, Mannis, ⊗4Mathematical Challenges⊗*, NCTM, Wahington, D.C., 1965.
Cohen, Paul J., ⊗4Set Theory and the Continuum Hypothesis⊗*, W.A.Benjamin, Inc.,
New York, 1966.
Copeland, Richard W., ⊗4How Children Learn Mathematics⊗*, The MacMillan
Company, London, 1970.
Courant, Richard, and Robins, Herbert, ⊗4What is Mathematics⊗*,
Oxford University Press, New York, 1941.
D'Augustine, Charles, ⊗4Multiple Methods of Teaching Mathematics in the
Elementary School⊗*, Harper & Row, New York, 1968.
Dornbusch, Sanford, and Scott, ⊗4Evaluation and the Exercise of Authority⊗*,
Jossey-Bass, San Francisco, 1975.
Douglas, Mary (ed.), ⊗4Rules and Meanings⊗*, Penguin Education,
Baltimore, Md., 1973.
Dowdy, S. M., ⊗4Mathematics: Art and Science⊗*, John Wiley & Sons, NY, 1971.
Dubin, Robert, ⊗4Theory Building⊗*, The Free Press, New York, 1969.
Dubs, Homer H., ⊗4Rational Induction⊗*, U. of Chicago Press, Chicago, 1930.
Dudley, Underwood, ⊗4Elementary Number Theory⊗*, W. H. Freeman and
Company, San Francisco, 1969.
Eynden, Charles Vanden, ⊗4Number Theory: An Introduction to Proof⊗*,
International Textbook Comapny, Scranton, Pennsylvania, 1970.
Fuller, R. Buckminster, ⊗4Intuition⊗*, Doubleday, Garden City, New York,
1972.
GCMP, ⊗4Key Topics in Mathematics⊗*, Science Research Associates,
Palo Alto, 1965.
Goldstein, Ira, ⊗4Elementary Geometry Theorem Proving⊗*, MIT AI Memo 280,
April, 1973.
Goodstein, R. L., ⊗4Fundamental Concepts of Mathematics⊗*, Pergamon Press,
New York, 1962.
Goodstein, R. L., ⊗4Recursive Number Theory⊗*, North-Holland Publishing Co.,
Amsterdam, 1964.
@Green, Waldinger, Barstow, Elschlager, Lenat, McCune, Shaw, and Steinberg,
⊗4Progress Report on Program-Understanding Systems⊗*, Memo AIM-240,
CS Report STAN-CS-74-444,Artificial Intelligence Laboratory,
Stanford University, August, 1974.
@Hadamard, Jaques, ⊗4The Psychology of Invention in the Mathematical
Field⊗*, Dover Publications, New York, 1945.
Halmos, Paul R., ⊗4Naive Set Theory⊗*, D. Van Nostrand Co.,
Princeton, 1960.
Hanson, Norwood R., ⊗4Perception and Discovery⊗*, Freeman, Cooper & Co.,
San Francisco, 1969.
Hartman, Robert S., ⊗4The Structure of Value: Foundations of Scientific
Axiology⊗*, Southern Illinois University Press, Carbondale, Ill., 1967.
Hempel, Carl G., ⊗4Fundamentals of Concept Formation in Empirical
Science⊗*, University of Chicago Press, Chicago, 1952.
Hibben, John Grier, ⊗4Inductive Logic⊗*, Charles Scribner's Sons,
New York, 1896.
Hilpinen, Risto, ⊗4Rules of Acceptance and Inductive Logic⊗*, Acta
Philosophica Fennica, Fasc. 22, North-Holland Publishing Company,
Amsterdam, 1968.
Hintikka, Jaako, ⊗4Knowledge and Belief⊗*, Cornell U. Press, Ithaca, NY, 1962.
Hintikka, Jaako, and Suppes, Patrick (eds.), ⊗4Aspects of Inductive
Logic⊗*, North-Holland Publishing Company, Amsterdam, 1966.
Jouvenal, Bertrand de, ⊗4The Art of Conjecture⊗*, Basic Books, Inc.,
New York, 1967.
@Kershner, R.B., and L.R.Wilcox, ⊗4The Anatomy of Mathematics⊗*, The Ronald
Press Company, New York, 1950.
Klauder, Francis J., ⊗4The Wonder of Intelligence⊗*, Christopher
Publishing House, North QUincy, Mass., 1973.
Klerner, M., and J. Reinfeld, eds., ⊗4Interactive Systems for Applied Mathematics⊗*,
ACM Symposium, held in Washington, D.C., AUgust, 1967. Academic Press, NY, 1968.
Kline, M. (ed), ⊗4Mathematics in the Modern World: Readings from Scientific
American⊗*, W.H.Freeman and Co., San Francisco, 1968.
@Kling, Robert Elliot, ⊗4Reasoning by Analogy with Applications to Heuristic
Problem Solving: A Case Study⊗*, Stanford Artificial Intelligence Project
Memo AIM-147, CS Department report CS-216, August, 1971.
Koestler, Arthur, ⊗4The Act of Creation⊗*, New York, Dell Pub., 1967.
Korner, Stephan, ⊗4Conceptual Thinking⊗*, Dover Publications, New York,
1959.
Krivine, Jean-Louis, ⊗4Introduction to Axiomatic Set Theory⊗*, Humanities Press,
New York, 1971.
Kubinski, Tadeusz, ⊗4On Structurality of Rules of Inference⊗*, Prace
Wroclawskiego Towarzystwa Naukowego, Seria A, Nr. 107, Worclaw,
Poland, 1965.
Lakatos, Imre (ed.), ⊗4The Problem of Inductive Logic⊗*, North-Holland
Publishing Co., Amsterdam, 1968.
Lamon, William E., ⊗4Learning and the Nature of Mathematiccs⊗*, Science
Research Associates, Palo Alto, 1972.
Lang, Serge, ⊗4Algebra⊗*, Addison-Wesley, Menlo Park, 1971.
Lefrancois, Guy R., ⊗4Psychological Theories and Human Learning⊗*, 1972.
Le Lionnais, F., ⊗4Great Currents of Mathematical Thought⊗*, Dover
Publications, New York, 1971.
Margenau, Henry, ⊗4Integrative Principles of Modern Thought⊗*, Gordon
and Breach, New York, 1972.
Martin, James, ⊗4Design of Man-Computer Dialogues⊗*, Prentice-Hall, Inc.,
Englewood Cliffs, N. J., 1973.
Martin, R. M., ⊗4Toward a Systematic Pragmatics⊗*, North Holland Publishing
Company, Amsterdam, 1959.
Mendelson, Elliott, ⊗4Introduction to Mathematical Logic⊗*, Van Nostrand Reinhold
Company, New York, 1964.
Meyer, Jerome S., ⊗4Fun With Mathematics⊗*, Fawcett Publications,
Greenwich, Connecticut, 1952.
Mirsky, L., ⊗4Studies in Pure Mathematics⊗*, Academic Press, New
York, 1971.
Moore, Robert C., ⊗4D-SCRIPT: A Computational Theory of Descriptions⊗*,
MIT AI Memo 278, February, 1973.
National Council of Teachers of Mathematics, ⊗4The Growth of Mathematical
Ideas⊗*, 24th yearbook, NCTM, Washington, D.C., 1959.
Newell, Allen, and Simon, Herbert, ⊗4Human Problem Solving⊗*, 1972.
Nevins, Arthur J., ⊗4A Human Oriented Logic for Automatic Theorem
Proving⊗*, MIT AI Memo 268, October, 1972.
Niven, Ivan, and Zuckerman, Herbert, ⊗4An Introduction to the Theory
of Numbers⊗*, John Wiley & Sons, Inc., New York, 1960.
Olson, Robert G., ⊗4Meaning and Argument⊗*, Harcourt, Brace & World,
New York, 1969.
Ore, Oystein, ⊗4Number Theory and its History⊗*, McGraw-Hill,
New York, 1948.
Pietarinen, Juhani, ⊗4Lawlikeness, Analogy, and Inductive Logic⊗*,
North-Holland, Amsterdam, published as v. 26 of the series
Acta Philosophica Fennica (J. Hintikka, ed.), 1972.
@Poincare', Henri, ⊗4The Foundations of Science: Science and Hypothesis,
The Value of Science, Science and Method⊗*, The Science Press, New York,
1929.
.COMMENT main library, 501 P751F, copy 4;
@Polya, George, ⊗4Mathematics and Plausible Reasoning⊗*, Princeton
University Press, Princeton, Vol. 1, 1954; Vol. 2, 1954.
@Polya, George, ⊗4How To Solve It⊗*, Second Edition, Doubleday Anchor Books,
Garden City, New York, 1957.
@Polya, George, ⊗4Mathematical Discovery⊗*, John Wiley & Sons,
New York, Vol. 1, 1962; Vol. 2, 1965.
Richardson, Robert P., and Edward H. Landis, ⊗4Fundamental Conceptions of
Modern Mathematics⊗*, The Open Court Publishing Company, Chicago, 1916.
Rosskopf, Steffe, Taback (eds.), ⊗4Piagetian Cognitive-
Development Research and Mathematical Education⊗*,
National Council of Teachers of Mathematics, New York, 1971.
Rulison, Jeff, and... ⊗4QA4, A Procedural Frob...⊗*,
Technical Note..., Artificial Intelligence Center, SRI, Menlo
Park, California, ..., 1973.
Saaty, Thomas L., and Weyl, F. Joachim (eds.), ⊗4The Spirit and the Uses
of the Mathematical Sciences⊗*, McGraw-Hill Book Company, New York, 1969.
Schminke, C. W., and Arnold, William R., eds., ⊗4Mathematics is a Verb⊗*,
The Dryden Press, Hinsdale, Illinois, 1971.
Singh, Jagjit, ⊗4Great Ideas of Modern Mathematics⊗*, Dover Publications,
New York, 1959.
@Skemp, Richard R., ⊗4The Psychology of Learning Mathematics⊗*,
Penguin Books, Ltd., Middlesex, England, 1971.
Slocum, Jonathan, ⊗4The Graph-Processing Language GROPE⊗*, U. Texas at Austin,
Technical Report NL-22, August, 1974.
Smith, Nancy Woodland, ⊗4A Question-Answering System for Elementary Mathematics⊗*,
Stanford Institute for Mathematical Studies in the Social Sciences, Technical
Report 227, April 19, 1974.
Smith, R.L., Nancy Smith, and F.L. Rawson, ⊗4CONSTRUCT: In Search of a Theory of
Meaning⊗*, Stanford IMSSS Technical Report 238, October 25, 1974.
Stein, Sherman K., ⊗4Mathematics: The Man-Made Universe: An Introduction
to the Spirit of Mathematics⊗*, Second Edition, W. H. Freeman and
Company, San Francisco, 1969.
Stewart, B. M., ⊗4Theory of Numbers⊗*, The MacMillan Co., New York, 1952.
Stokes, C. Newton, ⊗4Teaching the Meanings of Arithmetic⊗*,
Appleton-Century-Crofts, New York, 1951.
Suppes, Patrick, ⊗4A Probabilistic Theory
of Causality⊗*, Acta Philosophica Fennica,
Fasc. 24, North-Holland Publishing Company, Amsterdam, 1970.
Teitelman, Warren, ⊗4INTERLISP Reference
Manual⊗*, XEROX PARC, 1974.
Venn, John, ⊗4The Principles of Empirical or Inductive Logic⊗*,
MacMillan and Co., London, 1889.
Waismann, Friedrich, ⊗4Introduction to Mathematical Thinking⊗*,
Frederick Ungar Publishing Co., New York, 1951.
Wickelgren, Wayne A., ⊗4How to Solve Problems: Elements of a Theory of Problems
and Problem Solving⊗*, W. H. Freeman and Co., Sanf Francisco, 1974.
Wilder, Raymond L., ⊗4Evolution of Mathematical Concepts⊗*, John Wiley & Sons,
Inc., NY, 1968.
Winston, P., (ed.),
"New Progress in Artificial Intelligence",
⊗4MIT AI Lab Memo AI-TR-310⊗*, June, 1974.
Good summaries of work on Frames,
Demons, Hacker, Heterarchy, Dialogue, and Belief.
Wittner, George E., ⊗4The Structure of Mathematics⊗*, Xerox College Publishing,
Lexington, Mass, 1972.
Wright, Georg H. von, ⊗4A Treatise on Induction and Probability⊗*,
Routledge and Kegan Paul, London, 1951.
.END
.SKIP TO COLUMN 1
.ASSEC(Articles)
.BEGIN FILL SINGLE SPACE PREFACE 1 INDENT 0,4,0 TURN OFF "@"
Amarel, Saul, ⊗4On Representations of Problems of Reasoning about
Actions⊗*, Machine Intelligence 3, 1968, pp. 131-171.
Bledsoe, W. W., ⊗4Splitting and Reduction Heuristics in Automatic
Theorem Proving⊗*, Artificial Intelligence 2, 1971, pp. 55-77.
Bledsoe and Bruell, Peter, ⊗4A Man-Machine Theorem-Proving System⊗*,
Artificial Intelligence 5, 1974, 51-72.
Bourbaki, Nicholas, ⊗4The Architechture of Mathematics⊗*, American Mathematics
Monthly, v. 57, pp. 221-232, Published by the MAA, Albany, NY, 1950.
@Boyer, Robert S., and J. S. Moore, ⊗4Proving Theorems about LISP Functions⊗*,
JACM, V. 22, No. 1, January, 1975, pp. 129-144.
@Bruijn, N. G. de, ⊗4AUTOMATH, a language for mathematics⊗*, Notes taken by
Barry Fawcett, of Lecures given at the Seminare de mathematiques Superieurs,
University de Montreal, June, 1971. Stanford University Computer Science
Library report number is 005913.
@Buchanan, Feigenbaum, and Sridharan, ⊗4Heuristic Theory Formation⊗*,
Machine Intelligence 7, 1972, pp. 267-...
@Bundy, Alan, ⊗4Doing Arithmetic with Diagrams⊗*, 3rd IJCAI,
1973, pp. 130-138.
Daalen, D. T. van, ⊗4A Description of AUTOMATH and some aspects of its language
theory⊗*, in the Proceedings of the SYmposium on APL, Paris, December, 1973,
P. Braffort (ed). This volume also contains other, more detailed articles on this
project, by Bert Jutting and Ids Zanlevan.
Engelman, C., ⊗4MATHLAB: A Program for On-Line Assistance in Symbolic Computation⊗*,
in Proceedings of the FJCC, Volume 2, Spartan Books, 1965.
Engelman, C., ⊗4MATHLAB '68⊗*, in IFIP, Edinburgh, 1968.
Gardner, Martin, ⊗4Mathematical Games⊗*, Scientific American, numerous columns,
including especially: February, 1975.
Goldstine, Herman H., and J. von Neumann, ⊗4On the Principles of Large Scale
Computing Machines,⊗* pages 1:33 of Volumne 5 of A. H. Taub (ed), ⊗4The
Collected Works of John von Neumann⊗*, Pergamon Press, NY, 1963.
Guard, J. R., et al., ⊗4Semi-Automated Mathematics⊗*, JACM 16,
January, 1969, pp. 49-62.
Halmos, Paul R., ⊗4Innovation in Mathematics⊗*, in
Kline, M. (ed), ⊗4Mathematics in the Modern World: Readings from Scientific
American⊗*, W.H.Freeman and Co., San Francisco, 1968, pp. 6-13. Originally in
Scientific American, September, 1958.
Hasse, H., ⊗4Mathemakik als Wissenschaft, Kunst und Macht⊗*,
(Mathematics as Science, Art, and Power), Baden-Badeb, 1952.
@Hewitt, Carl, ⊗4A Universal Modular ACTOR Formalism for
Artificial Intelligence⊗*, Third International Joint Conference on
Artificial Intelligence,
1973, pp. 235-245.
Menges, Gunter, ⊗4Inference and Decision⊗*,
A Volume in ⊗4Selecta Statistica Canadiana⊗*,
John Wiley & Sons, New York, 1973, pp. 1-16.
Kling, Robert E., ⊗4A Paradigm for Reasoning by Analogy⊗*,
Artificial Intelligence 2, 1971, pp. 147-178.
Knuth,Donald E., ⊗4Ancient Babylonian Algorithms⊗*,
CACM 15, July, 1972, pp. 671-677.
Lee, Richard C. T., ⊗4Fuzzy Logic and the Resolution Principle⊗*,
JACM 19, January, 1972, pp. 109-119.
@Lenat, D., ⊗4BEINGs: Knowledge as Interacting Experts⊗*, 4th IJCAI, 1975.
McCarthy, John, and Hayes, Patrick, ⊗4Some Philosophical Problems
from the Standpoint of Artificial Intelligence⊗*, Machine Intelligence
4, 1969, pp. 463-502.
Martin, W., and Fateman, R., ⊗4The MACSYMA System⊗*, Second
Symposium on Symbolic and Algebraic Manipulation, 1971, pp. 59-75.
@Minsky, Marvin, ⊗4Frames⊗*, in (Winston) ⊗4Psychology of Computer
Vision⊗*, 1974.
Moore, J., and Newell, ⊗4How Can Merlin Understand?⊗*, Carnegie-Mellon University
Department of Computer Science "preprint", November 15, 1973.
@Neumann, J. von, ⊗4The Mathematician⊗*, in R.B. Heywood (ed), ⊗4The Works
of the Mind⊗*, U. Chicago Press, pp. 180-196, 1947.
Neumann, J. von, ⊗4The Computer and the Brain⊗*, Silliman Lectures, Yale U. Press,
1958.
Pager, David, ⊗4A Proposal for a Computer-based Interactive Scientific
Community⊗*, CACM 15, February, 1972, pp. 71-75.
Pager, David, ⊗4On the Problem of Communicating Complex Information⊗*,
CACM 16, May, 1973, pp. 275-281.
@Sloman, Aaron, ⊗4Interactions Between Philosophy and Artificial
Intelligence: The Role of Intuition and Non-Logical Reasoning in
Intelligence⊗*, Artificial Intelligence 2, 1971, pp. 209-225.
Sloman, Aaron, ⊗4On Learning about Numbers⊗*,...
Winston, Patrick, ⊗4Learning Structural Descriptions
from Examples⊗*, Ph.D. thesis, Dept. of Electrical Engineering,
TR-76, Project MAC, TR-231, MIT AI Lab, September, 1970.
.END
.ASSEC(Acknowledgements)
I owe a great debt of thanks to
Avra Cohn (my co-researcher) and Cordell Green (my adviser), both for the
input of new ideas and for the evaluation, channelling, and pruning of
my own. Stimulating discussions with many individuals have also left their mark;
let me mention: B. Buchanan, R. Floyd, D. Knuth, M. Lenat,
E. Sacerdoti, R. Waldinger,
R. Weyrauch,
and M. Wilber.
Let me also thank SRI, for providing computer time for this research.
.ONCE TURN OFF "@"
The application of BEINGs to an Automatic Programming task is described
in [Lenat], and it was problems with the domain of concept-formation-program-writing
that led to the AM project.
A more complete description of AM can be perused as SYS3[AM,AJC]@SU-AI.
The full body of knowledge we expect to provide to AM is found on
file GIVEN[AM,AJC]@SU-AI.
.COMMENT table of contents;
.EVERY HEADING(,,)
.PORTION CONTENTS
.NOFILL
.NARROW 6,8
.BEGIN CENTER
.GROUP SKIP 3
.SELECT 5
AUTOMATED THEORY FORMATION
IN MATHEMATICS
.SELECT 2
⊗4Summary as of: Thursday, May 1, 1975⊗*
Douglas B. Lenat
Artificial Intelligence Laboratory
Stanford University
.END
.PREFACE 10 MILLS
.TURN ON "{∞→"
.NARROW 7,7
.RECEIVE
.PAGE←0
.SELECT 1